src/help.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2003 University of Virginia,
   4 **         Massachusetts Institute of Technology
   5 **
   6 ** This program is free software; you can redistribute it and/or modify it
   7 ** under the terms of the GNU General Public License as published by the
   8 ** Free Software Foundation; either version 2 of the License, or (at your
   9 ** option) any later version.
  10 **
  11 ** This program is distributed in the hope that it will be useful, but
  12 ** WITHOUT ANY WARRANTY; without even the implied warranty of
  13 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  14 ** General Public License for more details.
  15 **
  16 ** The GNU General Public License is available from http://www.gnu.org/ or
  17 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  18 ** MA 02111-1307, USA.
  19 **
  20 ** For information on splint: info@splint.org
  21 ** To report a bug: splint-bug@splint.org
  22 ** For more information: http://www.splint.org
  23 */
  24 /*
  25 ** help.c
  26 */
  27
  28 # include "splintMacros.nf"
  29 # include "basic.h"
  30 # include "help.h"
  31
  32 static void
  33 describeVars (void)
  34 {
  35   llmsg (message
  36           ("larch path = %s (set by %s environment variable and -larchpath flag)",
  37            context_getLarchPath (), cstring_makeLiteralTemp (LARCH_PATH)));
  38   llmsglit ("   --- path used to find larch initialization files and LSL traits");
  39
  40   llmsg (message
  41           ("lcl import dir = %s (set by %s environment variable or -lclimportdir flag)",
  42            context_getLCLImportDir (), cstring_makeLiteralTemp (LCLIMPORTDIR)));
  43   llmsglit ("   --- directory containing lcl standard library files "
  44             "(import with < ... >)");;
  45
  46   llmsg (message
  47          ("system include path = %s (set by -systemdirs flag)", context_getString (FLG_SYSTEMDIRS)));
  48   llmsglit ("   --- if file is found on this path, it is treated as a system file for error reporting");
  49 }
  50
  51 static void
  52 printAnnotations (void)
  53 {
  54   llmsglit ("Annotations");
  55   llmsglit ("-----------");
  56   llmsglit ("");
  57   llmsglit ("Annotations are semantic comments that document certain "
  58             "assumptions about functions, variables, parameters, and types. ");
  59   llmsglit ("");
  60   llmsglit ("They may be used to indicate where the representation of a "
  61             "user-defined type is hidden, to limit where a global variable may "
  62             "be used or modified, to constrain what a function implementation "
  63             "may do to its parameters, and to express checked assumptions about "
  64             "variables, types, structure fields, function parameters, and "
  65             "function results.");
  66   llmsglit ("");
  67   llmsglit ("Annotations are introduced by \"/*@\". The role of the @ may be "
  68             "played by any printable character, selected using -commentchar <char>.");
  69   llmsglit ("");
  70   llmsglit ("Consult the User's Guide for descriptions of checking associated with each annotation.");
  71   llmsglit ("");
  72   llmsglit ("Globals: (in function declarations)");
  73   llmsglit ("   /*@globals <globitem>,+ @*/");
  74   llmsglit ("      globitem is an identifier, internalState or fileSystem");
  75   llmsglit ("");
  76   llmsglit ("Modifies: (in function declarations)");
  77   llmsglit ("   /*@modifies <moditem>,+ @*/");
  78   llmsglit ("      moditem is an lvalue");
  79   llmsglit ("   /*@modifies nothing @*/");
  80   llmsglit ("   /*@*/   (Abbreviation for no globals and modifies nothing.)");
  81   llmsglit ("");
  82   llmsglit ("Iterators:");
  83   llmsglit ("   /*@iter <identifier> (<parameter-type-list>) @*/ - declare an iterator");
  84   llmsglit ("");
  85   llmsglit ("Constants:");
  86   llmsglit ("   /*@constant <declaration> @*/ - declares a constant");
  87   llmsglit ("");
  88   llmsglit ("Alternate Types:");
  89   llmsglit ("   /*@alt <basic-type>,+ @*/");
  90   llmsglit ("   (e.g., int /*@alt char@*/ is a type matching either int or char)");
  91   llmsglit ("");
  92   llmsglit ("Declarator Annotations");
  93   llmsglit ("");
  94   llmsglit ("Type Definitions:");
  95   llmsglit ("   /*@abstract@*/ - representation is hidden from clients");
  96   llmsglit ("   /*@concrete@*/ - representation is visible to clients");
  97   llmsglit ("   /*@immutable@*/ - instances of the type cannot change value");
  98   llmsglit ("   /*@mutable@*/ - instances of the type can change value");
  99   llmsglit ("   /*@refcounted@*/ - reference counted type");
 100   llmsglit ("");
 101   llmsglit ("Global Variables:");
 102   llmsglit ("   /*@unchecked@*/ - weakest checking for global use");
 103   llmsglit ("   /*@checkmod@*/ - check modification by not use of global");
 104   llmsglit ("   /*@checked@*/ - check use and modification of global");
 105   llmsglit ("   /*@checkedstrict@*/ - check use of global strictly");
 106   llmsglit ("");
 107   llmsglit ("Memory Management:");
 108   llmsglit ("   /*@dependent@*/ - a reference to externally-owned storage");
 109   llmsglit ("   /*@keep@*/ - a parameter that is kept by the called function");
 110   llmsglit ("   /*@killref@*/ - a refcounted parameter, killed by the call");
 111   llmsglit ("   /*@only@*/ - an unshared reference");
 112   llmsglit ("   /*@owned@*/ - owner of storage that may be shared by /*@dependent@*/ references");
 113   llmsglit ("   /*@shared@*/ - shared reference that is never deallocated");
 114   llmsglit ("   /*@temp@*/ - temporary parameter");
 115   llmsglit ("");
 116   llmsglit ("Aliasing:");
 117   llmsglit ("   /*@unique@*/ - may not be aliased by any other visible reference");
 118   llmsglit ("   /*@returned@*/ - may be aliased by the return value");
 119   llmsglit ("");
 120   llmsglit ("Exposure:");
 121   llmsglit ("   /*@observer@*/ - reference that cannot be modified");
 122   llmsglit ("   /*@exposed@*/ - exposed reference to storage in another object");
 123   llmsglit ("");
 124   llmsglit ("Definition State:");
 125   llmsglit ("   /*@out@*/ - storage reachable from reference need not be defined");
 126   llmsglit ("   /*@in@*/ - all storage reachable from reference must be defined");
 127   llmsglit ("   /*@partial@*/ - partially defined, may have undefined fields");
 128   llmsglit ("   /*@reldef@*/ - relax definition checking");
 129   llmsglit ("");
 130   llmsglit ("Global State: (for globals lists, no /*@, since list is already in /*@\'s)");
 131   llmsglit ("   undef - variable is undefined before the call");
 132   llmsglit ("   killed - variable is undefined after the call");
 133   llmsglit ("");
 134   llmsglit ("Null State:");
 135   llmsglit ("   /*@null@*/ - possibly null pointer");
 136   llmsglit ("   /*@notnull@*/ - definitely non-null pointer");
 137   llmsglit ("   /*@relnull@*/ - relax null checking");
 138   llmsglit ("");
 139   llmsglit ("Null Predicates:");
 140   llmsglit ("   /*@nullwhentrue@*/ - if result is TRUE, first parameter is NULL");
 141   llmsglit ("   /*@falsewhennull@*/ - if result is TRUE, first parameter is not NULL");
 142   llmsglit ("");
 143   llmsglit ("Execution:");
 144   llmsglit ("   /*@noreturn@*/ - function never returns");
 145   llmsglit ("   /*@maynotreturn@*/ - function may or may not return");
 146   llmsglit ("   /*@noreturnwhentrue@*/ - function does not return if first parameter is TRUE");
 147   llmsglit ("   /*@noreturnwhenfalse@*/ - function does not return if first parameter if FALSE");
 148   llmsglit ("   /*@alwaysreturns@*/ - function always returns");
 149   llmsglit ("");
 150   llmsglit ("Side-Effects:");
 151   llmsglit ("   /*@sef@*/ - corresponding actual parameter has no side effects");
 152   llmsglit ("");
 153   llmsglit ("Declaration:");
 154   llmsglit ("   /*@unused@*/ - need not be used (no unused errors reported)");
 155   llmsglit ("   /*@external@*/ - defined externally (no undefined error reported)");
 156   llmsglit ("");
 157   llmsglit ("Case:");
 158   llmsglit ("   /*@fallthrough@*/ - fall-through case");
 159   llmsglit ("");
 160   llmsglit ("Break:");
 161   llmsglit ("   /*@innerbreak@*/ - break is breaking an inner loop or switch");
 162   llmsglit ("   /*@loopbreak@*/ - break is breaking a loop");
 163   llmsglit ("   /*@switchbreak@*/ - break is breaking a switch");
 164   llmsglit ("   /*@innercontinue@*/ - continue is continuing an inner loop");
 165   llmsglit ("");
 166   llmsglit ("Unreachable Code:");
 167   llmsglit ("   /*@notreached@*/ - statement may be unreachable.");
 168   llmsglit ("");
 169   llmsglit ("Special Functions:");
 170   llmsglit ("   /*@printflike@*/ - check variable arguments like printf");
 171   llmsglit ("   /*@scanflike@*/ - check variable arguments like scanf");
 172 }
 173
 174 static void
 175 printComments (void)
 176 {
 177   llmsglit ("Control Comments");
 178   llmsglit ("----------------");
 179   llmsglit ("");
 180   llmsglit ("Setting Flags");
 181   llmsglit ("");
 182   llmsglit ("Most flags (all except those characterized as \"globally-settable only\") can be set locally using control comments. A control comment can set flags locally to override the command line settings. The original flag settings are restored before processing the next file.");
 183   llmsglit ("");
 184   llmsglit ("The syntax for setting flags in control comments is the same as that of the command line, except that flags may also be preceded by = to restore their setting to the original command-line value. For instance,");
 185   llmsglit ("   /*@+boolint -modifies =showfunc@*/");
 186   llmsglit ("sets boolint on (this makes bool and int indistinguishable types), sets modifies off (this prevents reporting of modification errors), and sets showfunc to its original setting (this controls  whether or not the name of a function is displayed before a message).");
 187   llmsglit ("");
 188   llmsglit ("Error Suppression");
 189   llmsglit ("");
 190   llmsglit ("Several comments are provided for suppressing messages. In general, it is usually better to use specific flags to suppress a particular error permanently, but the general error suppression flags may be more convenient for quickly suppressing messages for code that will be corrected or documented later.");
 191   llmsglit ("");
 192   llmsglit ("/*@ignore@*/ ... /*@end@*/");
 193   llgenindentmsgnoloc
 194     (cstring_makeLiteral
 195      ("No errors will be reported in code regions between /*@ignore@*/ and /*@end@*/. These comments can be used to easily suppress an unlimited number of messages."));
 196   llmsglit ("/*@i@*/");
 197     llgenindentmsgnoloc
 198     (cstring_makeLiteral
 199      ("No errors will be reported from an /*@i@*/ comment to the end of the line."));
 200   llmsglit ("/*@i<n>@*/");
 201   llgenindentmsgnoloc
 202     (cstring_makeLiteral
 203      ("No errors will be reported from an /*@i<n>@*/ (e.g., /*@i3@*/) comment to the end of the line. If there are not exactly n errors suppressed from the comment point to the end of the line, Splint will report an error."));
 204   llmsglit ("/*@t@*/, /*@t<n>@*/");
 205   llgenindentmsgnoloc
 206     (cstring_makeLiteral
 207      ("Like i and i<n>, except controlled by +tmpcomments flag. These can be used to temporarily suppress certain errors. Then, -tmpcomments can be set to find them again."));
 208   llmsglit ("");
 209   llmsglit ("Type Access");
 210   llmsglit ("");
 211   llmsglit ("/*@access <type>@*/");
 212   llmsglit ("   Allows the following code to access the representation of <type>");
 213   llmsglit ("/*@noaccess <type>@*/");
 214   llmsglit ("   Hides the representation of <type>");
 215   llmsglit ("");
 216   llmsglit ("Macro Expansion");
 217   llmsglit ("");
 218   llmsglit ("/*@notfunction@*/");
 219   llgenindentmsgnoloc
 220     (cstring_makeLiteral
 221      ("Indicates that the next macro definition is not intended to be a "
 222       "function, and should be expanded in line instead of checked as a "
 223       "macro function definition."));
 224 }
 225
 226 static void
 227 printFlags (void)
 228 {
 229   llmsglit ("Flag Categories");
 230   llmsglit ("---------------");
 231   listAllCategories ();
 232   llmsglit ("\nTo see the flags in a flag category, do\n   splint -help flags <category>");
 233   llmsglit ("To see a list of all flags in alphabetical order, do\n   splint -help flags alpha");
 234   llmsglit ("To see a full description of all flags, do\n   splint -help flags full");
 235 }
 236
 237 static void
 238 printMaintainer (void)
 239 {
 240   llmsg (message ("Maintainer: %s", cstring_makeLiteralTemp (PACKAGE_BUGREPORT)));
 241   llmsglit (COMPILE_INFO);
 242 }
 243
 244 static void
 245 printMail (void)
 246 {
 247   llmsglit ("Mailing Lists");
 248   llmsglit ("-------------");
 249   llmsglit ("");
 250   llmsglit ("There are two mailing lists associated with Splint: ");
 251   llmsglit ("");
 252   llmsglit ("   splint-announce@cs.virginia.edu");
 253   llmsglit ("");
 254   llmsglit ("      Reserved for announcements of new releases and bug fixes.");
 255   llmsglit ("");
 256   llmsglit ("   splint-discuss@virginia.edu");
 257   llmsglit ("");
 258   llmsglit ("      Informal discussions on the use and development of Splint.");
 259   llmsglit ("");
 260   llmsglit ("To subscribe or view archives, visit http://www.splint.org/lists.html");
 261 }
 262
 263 static void
 264 printReferences (void)
 265 {
 266   llmsglit ("References");
 267   llmsglit ("----------");
 268   llmsglit ("");
 269   llmsglit ("For more information, see the Splint web site: http://www.splint.org");
 270 }
 271
 272 static void
 273 describePrefixCodes (void)
 274 {
 275   llmsglit ("Prefix Codes");
 276   llmsglit ("------------");
 277   llmsglit ("");
 278   llmsglit ("These characters have special meaning in name prefixes:");
 279   llmsglit ("");
 280   llmsg (message ("   %h  Any uppercase letter [A-Z]", PFX_UPPERCASE));
 281   llmsg (message ("   %h  Any lowercase letter [a-z]", PFX_LOWERCASE));
 282   llmsg (message ("   %h  Any character (valid in a C identifier)", PFX_ANY));
 283   llmsg (message ("   %h  Any digit [0-9]", PFX_DIGIT));
 284   llmsg (message ("   %h  Any non-uppercase letter [a-z0-9_]", PFX_NOTUPPER));
 285   llmsg (message ("   %h  Any non-lowercase letter [A-Z0-9_]", PFX_NOTLOWER));
 286   llmsg (message ("   %h  Any letter [A-Za-z]", PFX_ANYLETTER));
 287   llmsg (message ("   %h  Any letter or digit [A-Za-z0-9]", PFX_ANYLETTERDIGIT));
 288   llmsglit ("   *  Zero or more repetitions of the previous character class until the end of the name");
 289 }
 290
 291 void help_showAvailableHelp (void)
 292 {
 293   showHerald ();
 294
 295   llmsg (message ("Source files are .c, .h and %s files.  If there is no suffix,",
 296                   LCL_EXTENSION));
 297   llmsg (message ("   Splint will look for <file>.c and <file>%s.", LCL_EXTENSION));
 298   llmsglit ("");
 299   llmsglit ("Use splint -help <topic or flag name> for more information");
 300   llmsglit ("");
 301   llmsglit ("Topics:");
 302   llmsglit ("");
 303   llmsglit ("   annotations (describes source-code annotations)");
 304   llmsglit ("   comments (describes control comments)");
 305   llmsglit ("   flags (describes flag categories)");
 306   llmsglit ("   flags <category> (describes flags in category)");
 307   llmsglit ("   flags all (short description of all flags)");
 308   llmsglit ("   flags alpha (list all flags alphabetically)");
 309   llmsglit ("   flags full (full description of all flags)");
 310   llmsglit ("   mail (information on mailing lists)");
 311   llmsglit ("   modes (show mode settings)");
 312   llmsglit ("   parseerrors (help on handling parser errors)");
 313   llmsglit ("   prefixcodes (character codes in namespace prefixes)");
 314   llmsglit ("   references (sources for more information)");
 315   llmsglit ("   vars (environment variables)");
 316   llmsglit ("   version (information on compilation, maintainer)");
 317   llmsglit ("");
 318 }
 319
 320 static bool
 321 specialFlagsHelp (char *next)
 322 {
 323   if ((next != NULL) && (*next != '-') && (*next != '+'))
 324     {
 325       if (mstring_equal (next, "alpha"))
 326         {
 327           printAlphaFlags ();
 328           return TRUE;
 329         }
 330       else if (mstring_equal (next, "all"))
 331         {
 332           printAllFlags (TRUE, FALSE);
 333           return TRUE;
 334         }
 335       else if (mstring_equal (next, "categories")
 336                || mstring_equal (next, "cats"))
 337         {
 338           listAllCategories ();
 339           return TRUE;
 340         }
 341       else if (mstring_equal (next, "full"))
 342         {
 343           printAllFlags (FALSE, TRUE);
 344           return TRUE;
 345         }
 346       else if (mstring_equal (next, "manual"))
 347         {
 348           printFlagManual (FALSE);
 349           return TRUE;
 350         }
 351       else if (mstring_equal (next, "webmanual"))
 352         {
 353           printFlagManual (TRUE);
 354           return TRUE;
 355         }
 356       else
 357         {
 358           return FALSE;
 359         }
 360     }
 361   else
 362     {
 363       return FALSE;
 364     }
 365 }
 366
 367 static void
 368 printParseErrors (void)
 369 {
 370   llmsglit ("Parse Errors");
 371   llmsglit ("------------");
 372   llmsglit ("");
 373   llmsglit ("Splint will sometimes encounter a parse error for code that "
 374             "can be parsed with a local compiler. There are a few likely "
 375             "causes for this and a number of techniques that can be used "
 376             "to work around the problem.");
 377   llmsglit ("");
 378   llmsglit ("Compiler extensions --- compilers sometimes extend the C "
 379             "language with compiler-specific keywords and syntax. While "
 380             "it is not advisible to use these, oftentimes one has no choice "
 381             "when the system header files use compiler extensions. ");
 382   llmsglit ("");
 383   llmsglit ("Splint supports some of the GNU (gcc) compiler extensions, "
 384             "if the +gnuextensions flag is set. You may be able to workaround "
 385             "other compiler extensions by using a pre-processor define. "
 386             "Alternately, you can surround the unparseable code with");
 387   llmsglit ("");
 388   llmsglit ("   # ifndef S_SPLINT_S");
 389   llmsglit ("   ...");
 390   llmsglit ("   # endif");
 391   llmsglit ("");
 392   /* evans 2000-12-21 fixed typo reported by Jeroen Ruigrok/Asmodai */
 393   llmsglit ("Missing type definitions --- an undefined type name will usually "
 394             "lead to a parse error. This often occurs when a standard header "
 395             "file defines some type that is not part of the standard library. ");
 396   llmsglit ("By default, Splint does not process the local files corresponding "
 397             "to standard library headers, but uses a library specification "
 398             "instead so dependencies on local system headers can be detected. "
 399             "If another system header file that does not correspond to a "
 400             "standard library header uses one of these superfluous types, "
 401             "a parse error will result.");
 402   llmsglit ("");
 403   llmsglit ("If the parse error is inside a posix standard header file, the "
 404             "first thing to try is +posixlib. This makes Splint use "
 405             "the posix library specification instead of reading the posix "
 406             "header files.");
 407   llmsglit ("");
 408   llmsglit ("Otherwise, you may need to either manually define the problematic "
 409             "type (e.g., add -Dmlink_t=int to your .splintrc file) or force "
 410             "splint to process the header file that defines it. This is done "
 411             "by setting -skipstdheaders or -skipposixheaders before "
 412             "the file that defines the type is #include'd.");
 413   llmsglit ("(See splint -help "
 414             "skipstdheaders and splint -help skipposixheaders for a list of "
 415             "standard headers.)  For example, if <sys/local.h> uses a type "
 416             "defined by posix header <sys/types.h> but not defined by the "
 417             "posix library, we might do: ");
 418   llmsglit ("");
 419   llmsglit ("   /*@-skipposixheaders@*/");
 420   llmsglit ("   # include <sys/types.h>");
 421   llmsglit ("   /*@=skipposixheaders@*/");
 422   llmsglit ("   # include <sys/local.h>");
 423   llmsglit ("");
 424   llmsglit ("to force Splint to process <sys/types.h>.");
 425   llmsglit ("");
 426   llmsglit ("At last resort, +trytorecover can be used to make Splint attempt "
 427             "to continue after a parse error.  This is usually not successful "
 428             "and the author does not consider assertion failures when +trytorecover "
 429             "is used to be bugs.");
 430 }
 431
 432 void help_processFlags (int argc, char **argv)
 433 {
 434   int i;
 435
 436   showHerald ();
 437
 438   if (argc == 0)
 439     {
 440       help_showAvailableHelp ();
 441     }
 442
 443   for (i = 0; i < argc; i++)
 444     {
 445       char *thisarg = argv[i];
 446
 447       if (*thisarg == '-' || *thisarg == '+')
 448         {
 449           thisarg++;    /* skip '-' */
 450         }
 451       if (mstring_equal (thisarg, "modes"))
 452         {
 453           llmsg (describeModes ());
 454         }
 455       else if (mstring_equal (thisarg, "vars")
 456                || mstring_equal (thisarg, "env"))
 457         {
 458           describeVars ();
 459         }
 460       else if (mstring_equal (thisarg, "annotations"))
 461         {
 462           printAnnotations ();
 463         }
 464       else if (mstring_equal (thisarg, "parseerrors"))
 465         {
 466           printParseErrors ();
 467         }
 468       else if (mstring_equal (thisarg, "comments"))
 469         {
 470           printComments ();
 471         }
 472       else if (mstring_equal (thisarg, "prefixcodes"))
 473         {
 474           describePrefixCodes ();
 475         }
 476       else if (mstring_equal (thisarg, "references")
 477                || mstring_equal (thisarg, "refs"))
 478         {
 479           printReferences ();
 480         }
 481       else if (mstring_equal (thisarg, "mail"))
 482         {
 483           printMail ();
 484         }
 485       else if (mstring_equal (thisarg, "maintainer")
 486                || mstring_equal (thisarg, "version"))
 487         {
 488           printMaintainer ();
 489         }
 490       else if (flags_isModeName (cstring_fromChars (thisarg)))
 491         {
 492           llmsg (describeMode (cstring_fromChars (thisarg)));
 493         }
 494       else if (mstring_equal (thisarg, "flags"))
 495         {
 496           if (i + 1 < argc)
 497             {
 498               char *next = argv[i + 1];
 499
 500               if (specialFlagsHelp (next))
 501                 {
 502                   i++;
 503                 }
 504               else
 505                 {
 506                   flagkind k = identifyCategory (cstring_fromChars (next));
 507
 508                   if (k != FK_NONE)
 509                     {
 510                       printCategory (k);
 511                       i++;
 512                     }
 513                 }
 514             }
 515           else
 516             {
 517               printFlags ();
 518             }
 519         }
 520       else
 521         {
 522           cstring s = describeFlag (cstring_fromChars (thisarg));
 523
 524           if (cstring_isDefined (s))
 525             {
 526               llmsg (s);
 527             }
 528         }
 529     }
 530 }