/*@notfunction@*/
# define globalExtraArgFlag FALSE, FALSE, TRUE, FALSE, ARG_SPECIAL
/*@notfunction@*/
-# define globalFileFlag FALSE, FALSE, TRUE, FALSE, ARG_FILE
+# define globalFileFlag FALSE, TRUE, TRUE, FALSE, ARG_FILE
/*@=namechecks@*/
/*
"a possibly null pointer.",
0, 0
},
+ {
+ FK_NULL, FK_MEMORY, plainFlag,
+ "nullinit",
+ FLG_NULLINIT,
+ "inconsistent initialization involving null pointer",
+ "A reference with no null annotation is initialized "
+ "to NULL. Use /*@null@*/ to declare the reference as "
+ "a possibly null pointer.",
+ 0, 0
+ },
/*
** Undefined Values (Section 3)
FK_OPS, FK_NONE, modeFlag,
"realcompare",
FLG_REALCOMPARE,
- "dangerous comparison between reals (dangerous because of inexact "
+ "dangerous equality comparison between reals (dangerous because of inexact "
+ "floating point representations)",
+ "Two real (float, double, or long double) values are compared "
+ "directly using == or != primitive. "
+ "This may produce unexpected results since floating point "
+ "representations are inexact. Instead, compare the difference to "
+ "FLT_EPSILON or DBL_EPSILON.",
+ 0, 0,
+ },
+ {
+ FK_OPS, FK_NONE, modeFlag,
+ "realrelatecompare",
+ FLG_REALRELATECOMPARE,
+ "possibly dangerous relational comparison between reals (dangerous because of inexact "
"floating point representations)",
"Two real (float, double, or long double) values are compared "
- "directly using a C primitive. "
+ "directly using < or >. "
"This may produce unexpected results since floating point "
"representations are inexact. Instead, compare the difference to "
"FLT_EPSILON or DBL_EPSILON.",
FK_BOOL, FK_NONE, regStringFlag, ARG_STRING,
"boolfalse",
FLG_BOOLFALSE,
- "set name of boolean false (default FALSE)",
+ "set name of boolean false (default false)",
NULL, 0, 0
},
{
FK_BOOL, FK_NONE, regStringFlag, ARG_STRING,
"booltrue",
FLG_BOOLTRUE,
- "set name of boolean true (default TRUE)",
+ "set name of boolean true (default true)",
NULL, 0, 0
},
{
FK_BOOL, FK_OPS, modeFlag,
"boolcompare",
FLG_BOOLCOMPARE,
- "comparison between bools (dangerous because of multiple TRUE values)",
+ "comparison between bools (dangerous because of multiple true values)",
"Two bool values are compared directly using a C primitive. This "
"may produce unexpected results since all non-zero values are "
- "considered TRUE, so different TRUE values may not be equal. "
+ "considered true, so different true values may not be equal. "
"The file bool.h (included in splint/lib) provides bool_equal "
"for safe bool comparisons.", 0, 0
},
"An abstraction barrier is broken. If necessary, use /*@access <type>@*/ to allow access to an abstract type.",
0, 0
},
+ {
+ FK_ABSTRACT, FK_NONE, modeFlag,
+ "abstractcompare",
+ FLG_ABSTRACTCOMPARE,
+ "object equality comparison on abstract type operands",
+ "An object comparison (== or !=) is used on operands of abstract type.",
+ 0, 0
+ },
+
+ {
+ FK_ABSTRACT, FK_NONE, plainFlag,
+ "numabstract",
+ FLG_NUMABSTRACT,
+ "data abstraction barriers",
+ "An abstraction barrier involving a numabstract type is broken. If necessary, use /*@access <type>@*/ to allow access to a numabstract type.",
+ 0, 0
+ },
+ {
+ FK_ABSTRACT, FK_NONE, modeFlag,
+ "numabstractcast",
+ FLG_NUMABSTRACTCAST,
+ "numeric literal cast to numabstract type",
+ "A numeric literal is cast to a numabstract type.",
+ 0, 0
+ },
+ {
+ FK_ABSTRACT, FK_NONE, modeFlag,
+ "numabstractlit",
+ FLG_NUMABSTRACTLIT,
+ "numeric literal can used as numabstract type",
+ "To allow a numeric literal to be used as a numabstract type, use +numabstractlit.",
+ 0, 0
+ },
+ {
+ FK_ABSTRACT, FK_TYPEEQ, modeFlag,
+ "numabstractindex",
+ FLG_NUMABSTRACTINDEX,
+ "a numabstract type can be used to index an array",
+ "To allow numabstract types to index arrays, use +numabstractindex.",
+ 0, 0
+ },
+ {
+ FK_ABSTRACT, FK_NONE, modeFlag,
+ "numabstractprint",
+ FLG_NUMABSTRACTPRINT,
+ "a numabstract value is printed using %d format code",
+ "A numabstract value is printed usind %d format code in a printf.",
+ 0, 0
+ },
{
FK_ABSTRACT, FK_IMPLICIT, plainFlag,
"impabstract",
"warnmissingglobs",
FLG_WARNMISSINGGLOBALS,
"global variable used in modifies clause is not listed in globals list",
- "A global variable is used in the modifies clause, but it not listed in "
+ "A global variable is used in the modifies clause, but it is not listed in "
"the globals list. The variable will be added to the globals list.",
0, 0
},
},
{
FK_CONTROL, FK_NONE, plainFlag,
- "emptyreturn",
+ "emptyret",
FLG_EMPTYRETURN,
"empty return in function declared to return value",
NULL,
"casebreak",
FLG_CASEBREAK,
"non-empty case in a switch without preceding break",
- "Execution falls through from the previous case.", 0, 0
+ "Execution falls through from the previous case (use /*@fallthrough@*/ to mark fallthrough cases).", 0, 0
},
{
FK_CONTROL, FK_NONE, modeFlag,
"A possibly non-nullterminated string/memory is used/referenced as a nullterminated one.",
0, 0
},
-
{
FK_BOUNDS, FK_MEMORY, specialFlag,
"bounds",
"memory bounds checking (sets boundsread and boundswrite)",
"Memory read or write may be out of bounds of allocated storage.", 0, 0
},
+ {
+ FK_BOUNDS, FK_MEMORY, specialFlag,
+ "likelybounds",
+ FLG_LIKELYBOUNDS,
+ "memory bounds checking (sets likelyboundsread and likelyboundswrite)",
+ "Memory read or write may be out of bounds of allocated storage.", 0, 0
+ },
+ {
+ FK_BOUNDS, FK_MEMORY, modeFlag,
+ "likelyboundsread",
+ FLG_LIKELYBOUNDSREAD,
+ "likely out of bounds read",
+ "A memory read references memory beyond the allocated storage.",
+ 0, 0
+ },
+ {
+ FK_BOUNDS, FK_MEMORY, modeFlag,
+ "likelyboundswrite",
+ FLG_LIKELYBOUNDSWRITE,
+ "likely buffer overflow from an out of bounds write",
+ "A memory write may write to an address beyond the allocated buffer.",
+ 0, 0
+ },
+
{
FK_BOUNDS, FK_MEMORY, modeFlag,
"boundsread",
},
{
- FK_BOUNDS, FK_DISPLAY, modeFlag,
+ FK_BOUNDS, FK_DISPLAY, plainFlag,
"fcnpost",
FLG_FUNCTIONPOST,
"display function post conditions",
0, 0
},
{
- FK_BOUNDS, FK_DISPLAY, modeFlag,
+ FK_BOUNDS, FK_DISPLAY, plainFlag,
"redundantconstraints",
FLG_REDUNDANTCONSTRAINTS,
"display seemingly redundant constraints",
},
{
- FK_BOUNDS, FK_MEMORY, modeFlag,
- "implictconstraint",
- FLG_IMPLICTCONSTRAINT,
+ FK_BOUNDS, FK_MEMORY, plainFlag,
+ "impboundsconstraints",
+ FLG_IMPBOUNDSCONSTRAINTS,
"generate implicit constraints for functions",
NULL,
0, 0
},
/*drl7x added 4/29/01 */
{
- FK_BOUNDS, FK_MEMORY, modeFlag,
+ FK_BOUNDS, FK_MEMORY, plainFlag,
"orconstraint",
FLG_ORCONSTRAINT,
"use limited OR expressions to resolve constraints",
NULL,
0, 0
},
-
- {
- FK_BOUNDS, FK_MEMORY, modeFlag,
- "nullterminated",
- FLG_NULLTERMINATEDWARNING,
- "misuse of nullterminated allocation",
- "A user annotated non-nullterminated buffer is used/referenced as a nullterminated one.",
- 0, 0
- },
-
{
- FK_BOUNDS, FK_DISPLAY, modeFlag,
+ FK_BOUNDS, FK_DISPLAY, plainFlag,
"showconstraintparens",
FLG_PARENCONSTRAINT,
"display parentheses around constraint terms",
NULL,
0, 0
},
+ /*drl added 2/4/2002*/
{
- FK_BOUNDS, FK_DISPLAY, modeFlag,
+ FK_BOUNDS, FK_DISPLAY, plainFlag,
+ "boundscompacterrormessages",
+ FLG_BOUNDSCOMPACTERRORMESSAGES,
+ "Display fewer new lines in bounds checking error messages",
+ NULL,
+ 0, 0
+ },
+ {
+ FK_BOUNDS, FK_DISPLAY, plainFlag,
"showconstraintlocation",
FLG_CONSTRAINTLOCATION,
"display location for every constraint generated",
0, 0
}, /*drl added flag 4/26/01*/
+ { /* evans added 2003-06-08 */
+ FK_BOUNDS, FK_MEMORY, modeFlag,
+ "allocmismatch",
+ FLG_ALLOCMISMATCH,
+ "type conversion involves storage of non-divisble size",
+ NULL, 0, 0
+ },
+
/*
** 10. Extensible Checking
*/
},
{
FK_MACROS, FK_CONTROL, modeFlag,
- "macroreturn",
+ "macroret",
FLG_MACRORETURN,
"return statement in macro body",
"The body of a macro declared as a function uses a return statement. "
{
FK_NAMES, FK_ANSI, modeFlag,
"isoreserved",
- FLG_ANSIRESERVED,
+ FLG_ISORESERVED,
"external name conflicts with name reserved for system or standard library",
"External name is reserved for system use by ISO C99 standard.",
0, 0
{
FK_NAMES, FK_ANSI, modeFlag,
"isoreservedinternal",
- FLG_ANSIRESERVEDLOCAL,
+ FLG_ISORESERVEDLOCAL,
"internal name conflicts with name reserved for system or standard library",
"Internal name is reserved for system in ISO C99 standard (this should not be necessary unless you are worried about C library implementations that violate the standard and use macros).",
0, 0
NULL, 0, 0
},
{
- FK_LIBS, FK_INIT, globalFlag,
+ FK_LIBS, FK_INIT, idemGlobalFlag,
"isolib",
FLG_ANSILIB,
"use normal standard library",
0, 0
},
{
- FK_LIBS, FK_INIT, globalFlag,
+ FK_LIBS, FK_INIT, idemGlobalFlag,
"strictlib",
FLG_STRICTLIB,
"interpret standard library strictly",
0, 0
},
{
- FK_LIBS, FK_INIT, globalFlag,
+ FK_LIBS, FK_INIT, idemGlobalFlag,
"unixlib",
FLG_UNIXLIB,
"use UNIX (sort-of) standard library",
0, 0
},
{
- FK_LIBS, FK_INIT, globalFlag,
+ FK_LIBS, FK_INIT, idemGlobalFlag,
"unixstrictlib",
FLG_UNIXSTRICTLIB,
"use strict version of UNIX (sort-of) library",
0, 0
},
{
- FK_LIBS, FK_INIT, globalFlag,
+ FK_LIBS, FK_INIT, idemGlobalFlag,
"posixlib",
FLG_POSIXLIB,
"use POSIX standard library",
0, 0
},
{
- FK_LIBS, FK_INIT, globalFlag,
+ FK_LIBS, FK_INIT, idemGlobalFlag,
"posixstrictlib",
FLG_POSIXSTRICTLIB,
"use strict POSIX standard library",
0, 0
},
{
- FK_LIBS, FK_INIT, globalFlag,
+ FK_LIBS, FK_INIT, idemGlobalFlag,
"whichlib",
FLG_WHICHLIB,
"show standard library filename",
"Should use <stdarg.h> instead.",
0, 0
},
+ {
+ FK_HEADERS, FK_FILES, plainFlag,
+ "caseinsensitivefilenames",
+ FLG_CASEINSENSITIVEFILENAMES,
+ "file names are case insensitive (file.h and FILE.H are the same file)",
+ NULL, 0, 0
+ },
/* 14.2 Generating Libraries */
},
{
FK_DIRECT, FK_FILES, plainFlag,
- "skipansiheaders",
- FLG_SKIPANSIHEADERS,
+ "skipisoheaders",
+ FLG_SKIPISOHEADERS,
"prevent inclusion of header files in a system directory with "
"names that match standard ANSI headers. The symbolic information "
"in the standard library is used instead. Flag in effect only "
"set number of spaces to indent sub-messages",
NULL, 0, 0
},
+ {
+ FK_FORMAT, FK_DISPLAY, valueFlag,
+ "locindentspaces",
+ FLG_LOCINDENTSPACES,
+ "set number of spaces to indent sub-messages that start with file locations",
+ NULL, 0, 0
+ },
+ {
+ FK_FORMAT, FK_DISPLAY, plainFlag,
+ "showdeephistory",
+ FLG_SHOWDEEPHISTORY,
+ "show all available information about storage mentioned in warnings",
+ NULL, 0, 0
+ },
{
FK_FORMAT, FK_DISPLAY, plainFlag,
"showcolumn",
"show column number where error is found",
NULL, 0, 0
},
+ {
+ FK_FORMAT, FK_DISPLAY, plainFlag,
+ "showloadloc",
+ FLG_SHOWLOADLOC,
+ "show location information for load files",
+ NULL, 0, 0
+ },
+ {
+ FK_FORMAT, FK_DISPLAY, globalFileFlag,
+ "csv",
+ FLG_CSV,
+ "produce comma-separated values (CSV) warnings output file",
+ NULL, 0, 0
+ },
+ {
+ FK_FORMAT, FK_DISPLAY, plainFlag,
+ "csvoverwrite",
+ FLG_CSVOVERWRITE,
+ "overwrite exisiting CVS output file",
+ NULL, 0, 0
+ },
{
FK_FORMAT, FK_DISPLAY, plainFlag,
"parenfileformat",
"show column number where error is found",
NULL, 0, 0
},
+ {
+ FK_FORMAT, FK_DISPLAY, plainFlag,
+ "htmlfileformat",
+ FLG_HTMLFILEFORMAT,
+ "show file locations as links",
+ NULL, 0, 0
+ },
{
FK_FORMAT, FK_NONE, plainFlag,
"showfunc",
FK_SYNTAX, FK_PREPROC, plainFlag,
"preproc",
FLG_PREPROC,
- "preprocessing error", NULL,
+ "preprocessing error",
+ "Preprocessing error.",
0, 0
},
"A string literal is assigned to a char array too small to hold it.",
0, 0
},
+ {
+ FK_TYPE, FK_NONE, modeFlag,
+ "stringliteralnoroomfinalnull",
+ FLG_STRINGLITNOROOMFINALNULL,
+ "string literal leaves no room for null terminator",
+ "A string literal is assigned to a char array that is not big enough to hold the final null terminator. This may not be a problem because a null character has been explictedly included in the string literal using an escape sequence",
+ 0, 0
+ },
{
FK_TYPE, FK_NONE, modeFlag,
"stringliteralnoroom",
"To make enum and int types equivalent, use +enumint.",
0, 0
},
+ {
+ FK_TYPEEQ, FK_NONE, modeFlag,
+ "longint",
+ FLG_LONGINT,
+ "long int and int are equivalent",
+ "To make long int and int types equivalent, use +longint.",
+ 0, 0
+ },
+ {
+ FK_TYPEEQ, FK_NONE, modeFlag,
+ "shortint",
+ FLG_SHORTINT,
+ "short int and int are equivalent",
+ "To make short int and int types equivalent, use +shortint.",
+ 0, 0
+ },
{
FK_TYPEEQ, FK_NONE, modeFlag,
"floatdouble",
FK_TYPEEQ, FK_POINTER, plainFlag,
"zeroptr",
FLG_ZEROPTR,
- "tread 0 as a pointer",
+ "treat 0 as a pointer",
NULL, 0, 0
},
{
"suppress herald and error count",
NULL, 0, 0
},
+
+ /*
+ ** Default is to send messages, warnings and errors to stderr
+ */
+
+ {
+ FK_DISPLAY, FK_ERRORS, idemGlobalFlag,
+ "messagestreamstdout",
+ FLG_MESSAGESTREAMSTDOUT,
+ "send status messages to standard output stream",
+ NULL, 0, 0
+ },
{
- FK_DISPLAY, FK_ERRORS, plainFlag,
- "usestderr",
- FLG_USESTDERR,
- "send error messages to standard error (instead of standard out)",
+ FK_DISPLAY, FK_ERRORS, idemGlobalFlag,
+ "messagestreamstderr",
+ FLG_MESSAGESTREAMSTDERR,
+ "send status messages to standard error stream",
+ NULL, 0, 0
+ },
+ {
+ FK_DISPLAY, FK_ERRORS, globalStringFlag, ARG_FILE,
+ "messagestream",
+ FLG_MESSAGESTREAM,
+ "send status messages to <file>",
+ NULL, 0, 0
+ },
+
+ {
+ FK_DISPLAY, FK_ERRORS, idemGlobalFlag,
+ "warningstreamstdout",
+ FLG_WARNINGSTREAMSTDOUT,
+ "send warnings to standard output stream",
+ NULL, 0, 0
+ },
+ {
+ FK_DISPLAY, FK_ERRORS, idemGlobalFlag,
+ "warningstreamstderr",
+ FLG_WARNINGSTREAMSTDERR,
+ "send warnings to standard error stream",
+ NULL, 0, 0
+ },
+ {
+ FK_DISPLAY, FK_ERRORS, globalStringFlag, ARG_FILE,
+ "warningstream",
+ FLG_WARNINGSTREAM,
+ "send warnings to <file>",
NULL, 0, 0
},
+
+ {
+ FK_DISPLAY, FK_ERRORS, idemGlobalFlag,
+ "errorstreamstdout",
+ FLG_ERRORSTREAMSTDOUT,
+ "send fatal errors to standard output stream",
+ NULL, 0, 0
+ },
+ {
+ FK_DISPLAY, FK_ERRORS, idemGlobalFlag,
+ "errorstreamstderr",
+ FLG_ERRORSTREAMSTDERR,
+ "send fatal errors to standard error stream",
+ NULL, 0, 0
+ },
+ {
+ FK_DISPLAY, FK_ERRORS, globalStringFlag, ARG_FILE,
+ "errorstream",
+ FLG_ERRORSTREAM,
+ "send fatal errors to <file>",
+ NULL, 0, 0
+ },
+
+ {
+ FK_DISPLAY, FK_ERRORS, globalFlag,
+ "streamoverwrite",
+ FLG_STREAMOVERWRITE,
+ "warn and exit if a stream output file would overwrite an existing file",
+ NULL, 0, 0
+ },
+
+
{
FK_DISPLAY, FK_ERRORS, plainFlag,
"showsummary",
"show file names are they are processed",
NULL, 0, 0
},
+ {
+ FK_DISPLAY, FK_FILES, plainFlag,
+ "warnsysfiles",
+ FLG_WARNSYSFILES,
+ "Splint has been run on a system file, by default no errors are reported for system files. Use +systemdirerrors if you want splint to report errors in system files. A file is considered a system file if it is in a system directory or a subdirectory of a system directory. The sysdirs flag can be used to control the directories treated as system directories.",
+ NULL, 0, 0
+ },
{
FK_DISPLAY, FK_NONE, globalFlag,
"stats",
NULL, 0, 0
},
{
- FK_DEBUG, FK_BOUNDS, modeFlag,
+ FK_DEBUG, FK_BOUNDS, plainFlag,
"debugfcnconstraint",
FLG_DEBUGFUNCTIONCONSTRAINT,
"debug function constraints",
andersk / splint.git / blobdiff