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