2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2002 University of Virginia,
4 ** Massachusetts Institute of Technology
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.
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.
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.
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
28 # include "splintMacros.nf"
41 eval = context_getLarchPath ();
42 def = osd_getEnvironmentVariable (LARCH_PATH);
44 if (cstring_isDefined (def) ||
45 !cstring_equal (eval, cstring_fromChars (DEFAULT_LARCHPATH)))
47 llmsg (message ("LARCH_PATH = %s", eval));
51 llmsg (message ("LARCH_PATH = <not set> (default = %s)",
52 cstring_fromChars (DEFAULT_LARCHPATH)));
55 llmsglit (" --- path used to find larch initialization files and LSL traits");
57 eval = context_getLCLImportDir ();
58 def = osd_getEnvironmentVariable (cstring_makeLiteralTemp (LCLIMPORTDIR));
60 if (cstring_isDefined (def) ||
61 !cstring_equal (eval, cstring_fromChars (DEFAULT_LCLIMPORTDIR)))
63 llmsg (message ("%q = %s", cstring_makeLiteral (LCLIMPORTDIR), eval));
67 llmsg (message ("%s = <not set, default: %s>", cstring_makeLiteralTemp (LCLIMPORTDIR),
68 cstring_makeLiteralTemp (DEFAULT_LCLIMPORTDIR)));
71 llmsglit (" --- directory containing lcl standard library files "
72 "(import with < ... >)");;
75 ("include path = %q (set by environment variable %s and -I flags)",
76 cppReader_getIncludePath (), INCLUDEPATH_VAR));
78 llmsglit (" --- path used to find #include'd files");
81 ("systemdirs = %s (set by -systemdirs or environment variable %s)", /*@i413223@*/
82 context_getString (FLG_SYSTEMDIRS),
85 llmsglit (" --- if file is found on this path, it is treated as a system file for error reporting");
89 printAnnotations (void)
91 llmsglit ("Annotations");
92 llmsglit ("-----------");
94 llmsglit ("Annotations are semantic comments that document certain "
95 "assumptions about functions, variables, parameters, and types. ");
97 llmsglit ("They may be used to indicate where the representation of a "
98 "user-defined type is hidden, to limit where a global variable may "
99 "be used or modified, to constrain what a function implementation "
100 "may do to its parameters, and to express checked assumptions about "
101 "variables, types, structure fields, function parameters, and "
102 "function results.");
104 llmsglit ("Annotations are introduced by \"/*@\". The role of the @ may be "
105 "played by any printable character, selected using -commentchar <char>.");
107 llmsglit ("Consult the User's Guide for descriptions of checking associated with each annotation.");
109 llmsglit ("Globals: (in function declarations)");
110 llmsglit (" /*@globals <globitem>,+ @*/");
111 llmsglit (" globitem is an identifier, internalState or fileSystem");
113 llmsglit ("Modifies: (in function declarations)");
114 llmsglit (" /*@modifies <moditem>,+ @*/");
115 llmsglit (" moditem is an lvalue");
116 llmsglit (" /*@modifies nothing @*/");
117 llmsglit (" /*@*/ (Abbreviation for no globals and modifies nothing.)");
119 llmsglit ("Iterators:");
120 llmsglit (" /*@iter <identifier> (<parameter-type-list>) @*/ - declare an iterator");
122 llmsglit ("Constants:");
123 llmsglit (" /*@constant <declaration> @*/ - declares a constant");
125 llmsglit ("Alternate Types:");
126 llmsglit (" /*@alt <basic-type>,+ @*/");
127 llmsglit (" (e.g., int /*@alt char@*/ is a type matching either int or char)");
129 llmsglit ("Declarator Annotations");
131 llmsglit ("Type Definitions:");
132 llmsglit (" /*@abstract@*/ - representation is hidden from clients");
133 llmsglit (" /*@concrete@*/ - representation is visible to clients");
134 llmsglit (" /*@immutable@*/ - instances of the type cannot change value");
135 llmsglit (" /*@mutable@*/ - instances of the type can change value");
136 llmsglit (" /*@refcounted@*/ - reference counted type");
138 llmsglit ("Global Variables:");
139 llmsglit (" /*@unchecked@*/ - weakest checking for global use");
140 llmsglit (" /*@checkmod@*/ - check modification by not use of global");
141 llmsglit (" /*@checked@*/ - check use and modification of global");
142 llmsglit (" /*@checkedstrict@*/ - check use of global strictly");
144 llmsglit ("Memory Management:");
145 llmsglit (" /*@dependent@*/ - a reference to externally-owned storage");
146 llmsglit (" /*@keep@*/ - a parameter that is kept by the called function");
147 llmsglit (" /*@killref@*/ - a refcounted parameter, killed by the call");
148 llmsglit (" /*@only@*/ - an unshared reference");
149 llmsglit (" /*@owned@*/ - owner of storage that may be shared by /*@dependent@*/ references");
150 llmsglit (" /*@shared@*/ - shared reference that is never deallocated");
151 llmsglit (" /*@temp@*/ - temporary parameter");
153 llmsglit ("Aliasing:");
154 llmsglit (" /*@unique@*/ - may not be aliased by any other visible reference");
155 llmsglit (" /*@returned@*/ - may be aliased by the return value");
157 llmsglit ("Exposure:");
158 llmsglit (" /*@observer@*/ - reference that cannot be modified");
159 llmsglit (" /*@exposed@*/ - exposed reference to storage in another object");
161 llmsglit ("Definition State:");
162 llmsglit (" /*@out@*/ - storage reachable from reference need not be defined");
163 llmsglit (" /*@in@*/ - all storage reachable from reference must be defined");
164 llmsglit (" /*@partial@*/ - partially defined, may have undefined fields");
165 llmsglit (" /*@reldef@*/ - relax definition checking");
167 llmsglit ("Global State: (for globals lists, no /*@, since list is already in /*@\'s)");
168 llmsglit (" undef - variable is undefined before the call");
169 llmsglit (" killed - variable is undefined after the call");
171 llmsglit ("Null State:");
172 llmsglit (" /*@null@*/ - possibly null pointer");
173 llmsglit (" /*@notnull@*/ - definitely non-null pointer");
174 llmsglit (" /*@relnull@*/ - relax null checking");
176 llmsglit ("Null Predicates:");
177 llmsglit (" /*@nullwhentrue@*/ - if result is TRUE, first parameter is NULL");
178 llmsglit (" /*@falsewhennull@*/ - if result is TRUE, first parameter is not NULL");
180 llmsglit ("Execution:");
181 llmsglit (" /*@noreturn@*/ - function never returns");
182 llmsglit (" /*@maynotreturn@*/ - function may or may not return");
183 llmsglit (" /*@noreturnwhentrue@*/ - function does not return if first parameter is TRUE");
184 llmsglit (" /*@noreturnwhenfalse@*/ - function does not return if first parameter if FALSE");
185 llmsglit (" /*@alwaysreturns@*/ - function always returns");
187 llmsglit ("Side-Effects:");
188 llmsglit (" /*@sef@*/ - corresponding actual parameter has no side effects");
190 llmsglit ("Declaration:");
191 llmsglit (" /*@unused@*/ - need not be used (no unused errors reported)");
192 llmsglit (" /*@external@*/ - defined externally (no undefined error reported)");
195 llmsglit (" /*@fallthrough@*/ - fall-through case");
198 llmsglit (" /*@innerbreak@*/ - break is breaking an inner loop or switch");
199 llmsglit (" /*@loopbreak@*/ - break is breaking a loop");
200 llmsglit (" /*@switchbreak@*/ - break is breaking a switch");
201 llmsglit (" /*@innercontinue@*/ - continue is continuing an inner loop");
203 llmsglit ("Unreachable Code:");
204 llmsglit (" /*@notreached@*/ - statement may be unreachable.");
206 llmsglit ("Special Functions:");
207 llmsglit (" /*@printflike@*/ - check variable arguments like printf");
208 llmsglit (" /*@scanflike@*/ - check variable arguments like scanf");
214 llmsglit ("Control Comments");
215 llmsglit ("----------------");
217 llmsglit ("Setting Flags");
219 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 ("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,");
222 llmsglit (" /*@+boolint -modifies =showfunc@*/");
223 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 ("Error Suppression");
227 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 ("/*@ignore@*/ ... /*@end@*/");
232 ("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."));
233 llmsglit ("/*@i@*/");
236 ("No errors will be reported from an /*@i@*/ comment to the end of the line."));
237 llmsglit ("/*@i<n>@*/");
240 ("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."));
241 llmsglit ("/*@t@*/, /*@t<n>@*/");
244 ("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 ("Type Access");
248 llmsglit ("/*@access <type>@*/");
249 llmsglit (" Allows the following code to access the representation of <type>");
250 llmsglit ("/*@noaccess <type>@*/");
251 llmsglit (" Hides the representation of <type>");
253 llmsglit ("Macro Expansion");
255 llmsglit ("/*@notfunction@*/");
258 ("Indicates that the next macro definition is not intended to be a "
259 "function, and should be expanded in line instead of checked as a "
260 "macro function definition."));
266 llmsglit ("Flag Categories");
267 llmsglit ("---------------");
268 listAllCategories ();
269 llmsglit ("\nTo see the flags in a flag category, do\n splint -help flags <category>");
270 llmsglit ("To see a list of all flags in alphabetical order, do\n splint -help flags alpha");
271 llmsglit ("To see a full description of all flags, do\n splint -help flags full");
275 printMaintainer (void)
277 llmsg (message ("Maintainer: %s", cstring_makeLiteralTemp (SPLINT_MAINTAINER)));
278 llmsglit (LCL_COMPILE);
284 llmsglit ("Mailing Lists");
285 llmsglit ("-------------");
287 llmsglit ("There are two mailing lists associated with Splint: ");
289 llmsglit (" lclint-announce@virginia.edu");
291 llmsglit (" Reserved for announcements of new releases and bug fixes.");
292 llmsglit (" To subscribe, send a message to majordomo@virginia.edu with body: ");
293 llmsglit (" subscribe lclint-announce");
295 llmsglit (" lclint-interest@virginia.edu");
297 llmsglit (" Informal discussions on the use and development of Splint.");
298 llmsglit (" To subscribe, send a message to majordomo@virginia.edu with body: ");
299 llmsglit (" subscribe lclint-interest");
303 printReferences (void)
305 llmsglit ("References");
306 llmsglit ("----------");
308 llmsglit ("For more information, see the Splint web site: http://www.splint.org");
312 describePrefixCodes (void)
314 llmsglit ("Prefix Codes");
315 llmsglit ("------------");
317 llmsglit ("These characters have special meaning in name prefixes:");
319 llmsg (message (" %h Any uppercase letter [A-Z]", PFX_UPPERCASE));
320 llmsg (message (" %h Any lowercase letter [a-z]", PFX_LOWERCASE));
321 llmsg (message (" %h Any character (valid in a C identifier)", PFX_ANY));
322 llmsg (message (" %h Any digit [0-9]", PFX_DIGIT));
323 llmsg (message (" %h Any non-uppercase letter [a-z0-9_]", PFX_NOTUPPER));
324 llmsg (message (" %h Any non-lowercase letter [A-Z0-9_]", PFX_NOTLOWER));
325 llmsg (message (" %h Any letter [A-Za-z]", PFX_ANYLETTER));
326 llmsg (message (" %h Any letter or digit [A-Za-z0-9]", PFX_ANYLETTERDIGIT));
327 llmsglit (" * Zero or more repetitions of the previous character class until the end of the name");
330 void help_showAvailableHelp (void)
334 llmsg (message ("Source files are .c, .h and %s files. If there is no suffix,",
336 llmsg (message (" Splint will look for <file>.c and <file>%s.", LCL_EXTENSION));
338 llmsglit ("Use splint -help <topic or flag name> for more information");
340 llmsglit ("Topics:");
342 llmsglit (" annotations (describes source-code annotations)");
343 llmsglit (" comments (describes control comments)");
344 llmsglit (" flags (describes flag categories)");
345 llmsglit (" flags <category> (describes flags in category)");
346 llmsglit (" flags all (short description of all flags)");
347 llmsglit (" flags alpha (list all flags alphabetically)");
348 llmsglit (" flags full (full description of all flags)");
349 llmsglit (" mail (information on mailing lists)");
350 llmsglit (" modes (show mode settings)");
351 llmsglit (" parseerrors (help on handling parser errors)");
352 llmsglit (" prefixcodes (character codes in namespace prefixes)");
353 llmsglit (" references (sources for more information)");
354 llmsglit (" vars (environment variables)");
355 llmsglit (" version (information on compilation, maintainer)");
360 specialFlagsHelp (char *next)
362 if ((next != NULL) && (*next != '-') && (*next != '+'))
364 if (mstring_equal (next, "alpha"))
369 else if (mstring_equal (next, "all"))
371 printAllFlags (TRUE, FALSE);
374 else if (mstring_equal (next, "categories")
375 || mstring_equal (next, "cats"))
377 listAllCategories ();
380 else if (mstring_equal (next, "full"))
382 printAllFlags (FALSE, TRUE);
385 else if (mstring_equal (next, "manual"))
387 printFlagManual (FALSE);
390 else if (mstring_equal (next, "webmanual"))
392 printFlagManual (TRUE);
407 printParseErrors (void)
409 llmsglit ("Parse Errors");
410 llmsglit ("------------");
412 llmsglit ("Splint will sometimes encounter a parse error for code that "
413 "can be parsed with a local compiler. There are a few likely "
414 "causes for this and a number of techniques that can be used "
415 "to work around the problem.");
417 llmsglit ("Compiler extensions --- compilers sometimes extend the C "
418 "language with compiler-specific keywords and syntax. While "
419 "it is not advisible to use these, oftentimes one has no choice "
420 "when the system header files use compiler extensions. ");
422 llmsglit ("Splint supports some of the GNU (gcc) compiler extensions, "
423 "if the +gnuextensions flag is set. You may be able to workaround "
424 "other compiler extensions by using a pre-processor define. "
425 "Alternately, you can surround the unparseable code with");
427 llmsglit (" # ifndef S_SPLINT_S");
429 llmsglit (" # endif");
431 /* evans 2000-12-21 fixed typo reported by Jeroen Ruigrok/Asmodai */
432 llmsglit ("Missing type definitions --- an undefined type name will usually "
433 "lead to a parse error. This often occurs when a standard header "
434 "file defines some type that is not part of the standard library. ");
435 llmsglit ("By default, Splint does not process the local files corresponding "
436 "to standard library headers, but uses a library specification "
437 "instead so dependencies on local system headers can be detected. "
438 "If another system header file that does not correspond to a "
439 "standard library header uses one of these superfluous types, "
440 "a parse error will result.");
442 llmsglit ("If the parse error is inside a posix standard header file, the "
443 "first thing to try is +posixlib. This makes Splint use "
444 "the posix library specification instead of reading the posix "
447 llmsglit ("Otherwise, you may need to either manually define the problematic "
448 "type (e.g., add -Dmlink_t=int to your .splintrc file) or force "
449 "splint to process the header file that defines it. This is done "
450 "by setting -skipisoheaders or -skipposixheaders before "
451 "the file that defines the type is #include'd.");
452 llmsglit ("(See splint -help "
453 "skipisoheaders and splint -help skipposixheaders for a list of "
454 "standard headers.) For example, if <sys/local.h> uses a type "
455 "defined by posix header <sys/types.h> but not defined by the "
456 "posix library, we might do: ");
458 llmsglit (" /*@-skipposixheaders@*/");
459 llmsglit (" # include <sys/types.h>");
460 llmsglit (" /*@=skipposixheaders@*/");
461 llmsglit (" # include <sys/local.h>");
463 llmsglit ("to force Splint to process <sys/types.h>.");
465 llmsglit ("At last resort, +trytorecover can be used to make Splint attempt "
466 "to continue after a parse error. This is usually not successful "
467 "and the author does not consider assertion failures when +trytorecover "
468 "is used to be bugs.");
471 void help_processFlags (int argc, char **argv)
479 help_showAvailableHelp ();
482 for (i = 0; i < argc; i++)
484 char *thisarg = argv[i];
486 if (*thisarg == '-' || *thisarg == '+')
488 thisarg++; /* skip '-' */
490 if (mstring_equal (thisarg, "modes"))
492 llmsg (describeModes ());
494 else if (mstring_equal (thisarg, "vars")
495 || mstring_equal (thisarg, "env"))
499 else if (mstring_equal (thisarg, "annotations"))
503 else if (mstring_equal (thisarg, "parseerrors"))
507 else if (mstring_equal (thisarg, "comments"))
511 else if (mstring_equal (thisarg, "prefixcodes"))
513 describePrefixCodes ();
515 else if (mstring_equal (thisarg, "references")
516 || mstring_equal (thisarg, "refs"))
520 else if (mstring_equal (thisarg, "mail"))
524 else if (mstring_equal (thisarg, "maintainer")
525 || mstring_equal (thisarg, "version"))
529 else if (mstring_equal (thisarg, "flags"))
533 char *next = argv[i + 1];
535 if (specialFlagsHelp (next))
541 flagkind k = identifyCategory (cstring_fromChars (next));
557 cstring s = describeFlag (cstring_fromChars (thisarg));
559 if (cstring_isDefined (s))