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