Added check of user specified post conditions.

[splint.git] / src / flags.def

diff --git a/src/flags.def b/src/flags.def
index 2ac68654a08a33256234dba120a51e64c08a37d0..541d6bd64200422addf530a0aed45fdf149dc3a1 100644 (file)
--- a/src/flags.def
+++ b/src/flags.def
@@ -3,8 +3,9 @@
 ** flags.def
 **
 ** This file is used to generate the flag header files.
+**
+** Don't forget to regenerate flag_codes.gen. (lost the Makefile...bleech!)
 */
-
                             /* spec   idem   global  mode  args */
 /*@-namechecks@*/
 /*@notfunction@*/
@@ -52,13 +53,15 @@
 */
 
 static flaglist flags = {      
+  /* Deprecated 
 {      
   FK_ABSTRACT, FK_BOOL, plainFlag,
   "bool",
-  FLG_ABSTRACTBOOL,
+  F*//*Hide flag from makefile grep*//*LG_ABSTRACTBOOL,
   "boolean type is abstract",
   NULL, 0, 0
   },
+  */
 {
   FK_BOOL, FK_HELP, plainFlag,
   "likelybool",
@@ -1358,7 +1361,7 @@ static flaglist flags = {
   FK_IGNORERET, FK_BOOL, modeFlag,
   "retvalbool",
   FLG_RETVALBOOL,
-  "return value of type bool ignored",
+  "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
@@ -2764,6 +2767,83 @@ NULL, NULL,
   "A possibly non-nullterminated string/memory is used/referenced as a nullterminated one,  ",
   0, 0
 },
+{
+  FK_NT, FK_MEMORY, modeFlag,
+  "bufferoverflow",
+  FLG_BUFFEROVERFLOW,
+  "possible buffer overflow",
+  "A possibly buffer overflow has been detected,  ",
+  0, 0
+},
+{
+  FK_NT, FK_MEMORY, modeFlag,
+  "arrayread",
+  FLG_ARRAYREAD,
+  "possible out of bounds read",
+  "An array or pointer access references memory beyond the array or buffer,  ",
+  0, 0
+},
+{
+  FK_NT, FK_MEMORY, modeFlag,
+  "arraywrite",
+  FLG_ARRAYWRITE,
+  "possible buffer overflow from an out of bounds write",
+  "Memory is set past the end of an array or or after the allocated buffer,  ",
+  0, 0
+},
+  
+{
+  FK_NT, FK_MEMORY, modeFlag,
+  "fcnpost",
+  FLG_FUNCTIONPOST,
+  "Function has the post condition_Block Post condition:_This function block has the post condition ",
+  "LCLint has determined that the following statement true after the function,  ",
+  0, 0
+},
+{
+  FK_NT, FK_MEMORY, modeFlag,
+  "fcnconstraint",
+  FLG_FUNCTIONCONSTRAINT,
+    "unresolved constraint:",
+  "LCLint was unable to resolve a constraint at the top of the function.  If code is correct consider using explict annotation assertions,  ",
+  0, 0
+},
+    /*drl7x added 6/18/01 */    
+{
+  FK_NT, FK_MEMORY, modeFlag,
+  "checkpost",
+  FLG_CHECKPOST,
+  "unable to verify ensures annotation",
+  "LCLint was unable to determine that the function satisfies a post condition given in an ensures annotation,  ",
+  0, 0
+},
+
+{
+  FK_NT, FK_MEMORY, modeFlag,
+  "constraintlocation",
+  FLG_CONSTRAINTLOCATION,
+  "display full c expression for every constraint generated",
+  ",  ",
+  0, 0
+    },/*drl added flag 4/26/01*/
+{
+  FK_NT, FK_MEMORY, modeFlag,
+  "implictconstraint",
+  FLG_IMPLICTCONSTRAINT,
+  "Try to generate implicit constraints for functions",
+  ",  ",
+  0, 0
+},
+    /*drl7x added 4/29/01 */    
+{
+  FK_NT, FK_MEMORY, modeFlag,
+  "orconstraint",
+  FLG_ORCONSTRAINT,
+  "Use limited OR expressions to resolve constraints",
+  ",  ",
+  0, 0
+},
+    
 {
   FK_NT, FK_MEMORY, modeFlag,
   "nullterminated",
@@ -3297,6 +3377,13 @@ NULL, NULL,
   "0 is treated as a pointer",
   NULL, 0, 0
   },
+{
+  FK_TYPEEQ, FK_BOOL, modeFlag,
+  "zerobool",
+  FLG_ZEROBOOL,
+  "0 is treated as a boolean",
+  NULL, 0, 0
+  },
 {
   FK_UNRECOG, FK_DISPLAY, plainFlag,
   "repeatunrecog",