Merged with Dave Evans's changes.

[splint.git] / src / flags.def

diff --git a/src/flags.def b/src/flags.def
index bc448d5a69a66264e79e216e629624e61754b7fe..510acffe92cda6c33712e056b4e240a57e2fad80 100644 (file)
--- a/src/flags.def
+++ b/src/flags.def
@@ -2791,12 +2791,13 @@ NULL, NULL,
   "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",
-  "LCLint has determined that the following statement true after the function,  ",
+  "LCLint has determined that the following statement is true after the function,  ",
   0, 0
 },
 {
@@ -2807,6 +2808,16 @@ NULL, NULL,
   "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",