+ FK_IGNORERET, FK_BOOL, modeFlag,
+ "retvalother",
+ FLG_RETVALOTHER,
+ "return value of type other than bool or int ignored",
+ "Result returned by function call is not used. If this is intended, "
+ "can cast result to (void) to eliminate message.",
+ 0, 0
+ },
+ {
+ FK_IGNORERET, FK_BOOL, modeFlag,
+ "retvalbool",
+ FLG_RETVALBOOL,
+ "return value of manifest type bool ignored",
+ "Result returned by function call is not used. If this is intended, "
+ "can cast result to (void) to eliminate message.",
+ 0, 0
+ },
+ {
+ FK_IGNORERET, FK_NONE, modeFlag,
+ "retvalint",
+ FLG_RETVALINT,
+ "return value of type int ignored",
+ "Result returned by function call is not used. If this is intended, "
+ "can cast result to (void) to eliminate message.",
+ 0, 0
+ },
+
+ /*
+ ** 9. Buffer Sizes
+ */
+
+ {
+ FK_BOUNDS, FK_MEMORY, modeFlag,
+ "nullterminated",
+ FLG_NULLTERMINATED,
+ "misuse of nullterminated allocation",
+ "A possibly non-nullterminated string/memory is used/referenced as a nullterminated one.",
+ 0, 0
+ },
+ {
+ FK_BOUNDS, FK_MEMORY, specialFlag,
+ "bounds",
+ FLG_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, 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",
+ FLG_BOUNDSREAD,
+ "possible out of bounds read",
+ "A memory read references memory beyond the allocated storage.",
+ 0, 0
+ },
+ {
+ FK_BOUNDS, FK_MEMORY, plainFlag,
+ "boundswrite",
+ FLG_BOUNDSWRITE,
+ "possible 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_DISPLAY, plainFlag,
+ "fcnpost",
+ FLG_FUNCTIONPOST,
+ "display function post conditions",
+ "Display function post conditions.",
+ 0, 0
+ },
+ {
+ FK_BOUNDS, FK_DISPLAY, plainFlag,
+ "redundantconstraints",
+ FLG_REDUNDANTCONSTRAINTS,
+ "display seemingly redundant constraints",
+ "Display seemingly redundant constraints",
+ 0, 0
+ },
+ /*drl7x added 6/18/01 */
+ {
+ FK_BOUNDS, FK_MEMORY, modeFlag,
+ "checkpost",
+ FLG_CHECKPOST,
+ "unable to verify predicate in ensures clause",
+ "The function implementation may not satisfy a post condition given in an ensures clause.",
+ 0, 0
+ },
+
+ {
+ FK_BOUNDS, FK_MEMORY, plainFlag,
+ "implictconstraint",
+ FLG_IMPLICTCONSTRAINT,
+ "generate implicit constraints for functions",
+ NULL,
+ 0, 0
+ },
+ /*drl7x added 4/29/01 */
+ {
+ FK_BOUNDS, FK_MEMORY, plainFlag,
+ "orconstraint",
+ FLG_ORCONSTRAINT,
+ "use limited OR expressions to resolve constraints",
+ NULL,
+ 0, 0
+ },
+
+ {
+ FK_BOUNDS, FK_MEMORY, plainFlag,
+ "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, plainFlag,
+ "showconstraintparens",
+ FLG_PARENCONSTRAINT,
+ "display parentheses around constraint terms",
+ NULL,
+ 0, 0
+ },
+ /*drl added 2/4/2002*/
+ {
+ 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",
+ NULL,
+ 0, 0
+ }, /*drl added flag 4/26/01*/
+
+ /*
+ ** 10. Extensible Checking
+ */
+
+ {
+ FK_EXTENSIBLE, FK_FILES, globalStringFlag, ARG_FILE,
+ "mts",
+ FLG_MTSFILE,
+ "load meta state declaration and corresponding xh file",
+ NULL, 0, 0