/*@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)
"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,
"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, plainFlag,
+ "likely-boundsread",
+ FLG_LIKELYBOUNDSREAD,
+ "likely out of bounds read",
+ "A memory read references memory beyond the allocated storage.",
+ 0, 0
+ },
+ {
+ FK_BOUNDS, FK_MEMORY, plainFlag,
+ "likely-boundswrite",
+ 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, plainFlag,
"boundsread",
"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 */
"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",
"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
},
{