Made make lint work. Although exprNode_doSwitchExpr surpresses too much.

Splitt fcnconstraint and improved error messages.

diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h
index 40ab60ad283d8581f49f5a94067237f47c78ce21..225a79019da12923250ff92522b18197691e9dd6 100644 (file)
--- a/src/Headers/constraint.h
+++ b/src/Headers/constraint.h
@@ -38,13 +38,13 @@ extern void constraint_free (/*@only@*/  constraint p_c);
 /*@i22*/
 /*@-czechfcns*/
 
-extern constraint constraint_makeReadSafeExprNode ( /*@dependent@*/ /*@oberserver@*/ exprNode p_po, /*@dependent@*/ /*@oberserver@*/ exprNode p_ind);
+extern constraint constraint_makeReadSafeExprNode ( /*@dependent@*/ /*@observer@*/ exprNode p_po, /*@dependent@*/ /*@observer@*/ exprNode p_ind);
 
-extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (/*@dependent@*/ /*@oberserver@*/ exprNode p_po, /*@dependent@*/ /*@oberserver@*/ exprNode p_ind);
+extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (/*@dependent@*/ /*@observer@*/ exprNode p_po, /*@dependent@*/ /*@observer@*/ exprNode p_ind);
 
-extern /*@only@*/ constraint constraint_makeReadSafeInt (/*@dependent@*/ /*@oberserver@*/ exprNode p_t1, int p_index);
+extern /*@only@*/ constraint constraint_makeReadSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_t1, int p_index);
 
-extern /*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (/*@dependent@*/ /*@oberserver@*/ exprNode p_t1, /*@dependent@*/ /*@oberserver@*/ exprNode p_t2, fileloc p_sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (/*@dependent@*/ /*@observer@*/ exprNode p_t1, /*@dependent@*/ /*@observer@*/ exprNode p_t2, fileloc p_sequencePoint);
 
 extern void constraint_overWrite (constraint p_c1, /*@observer@*/ constraint p_c2) /*@modifies p_c1 @*/;
 
@@ -61,24 +61,24 @@ extern /*@only@*/ cstring constraint_unparse (/*@temp@*/ /*@observer@*/ constrai
 
 extern /*@only@*/ cstring constraint_print (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/;
 
-extern /*@only@*/ constraint constraint_makeWriteSafeInt (/*@dependent@*/ /*@oberserver@*/ exprNode p_po, int p_ind);
+extern /*@only@*/ constraint constraint_makeWriteSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_po, int p_ind);
 
 extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode p_dst, exprNode p_src) /*@modifies p_dst @*/;
 
-extern /*@only@*/ constraint constraint_makeEnsureEqual (/*@dependent@*/ /*@oberserver@*/ exprNode p_e1, /*@dependent@*/ /*@oberserver@*/ exprNode p_e2, fileloc p_sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
 
-extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (/*@dependent@*/ /*@oberserver@*/ exprNode p_e, fileloc p_sequencePoint);
+extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (/*@dependent@*/ /*@observer@*/ exprNode p_e, fileloc p_sequencePoint);
 
 extern constraint constraint_preserveOrig (/*@returned@*/ constraint p_c) /*@modifies p_c @*/;
 extern /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint p_precondition,
                                                            exprNodeList p_arglist);
 extern /*@only@*/ cstring  constraint_printDetailed (constraint p_c);
 
-extern /*@only@*/ constraint constraint_makeEnsureLessThan (/*@dependent@*/ /*@oberserver@*/ exprNode p_e1, /*@dependent@*/ /*@oberserver@*/ exprNode p_e2, fileloc p_sequencePoint);
-extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (/*@dependent@*/ /*@oberserver@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureLessThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
 
-extern /*@only@*/ constraint constraint_makeEnsureGreaterThan (/*@dependent@*/ /*@oberserver@*/ exprNode p_e1, /*@dependent@*/ /*@oberserver@*/ exprNode p_e2, fileloc p_sequencePoint);
-extern /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (/*@dependent@*/ /*@oberserver@*/ exprNode p_e1, /*@dependent@*/ /*@oberserver@*/ exprNode p_e2, fileloc p_sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureGreaterThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
 
 /*drl add 11/28/2000 */
 extern /*@only@*/ constraint constraint_makeSRefWriteSafeInt (sRef p_s, int p_ind);
@@ -93,9 +93,9 @@ extern /*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef p_s, long in
 
 extern /*@only@*/ constraint constraint_doFixResult (constraint p_postcondition, /*@dependent@*/ /*@observer@*/ exprNode p_fcnCall);
 
-extern /*@only@*/ constraint constraint_makeEnsureLteMaxRead(/*@dependent@*/ /*@oberserver@*/ exprNode p_index, /*@dependent@*/ /*@oberserver@*/ exprNode p_buffer);
+extern /*@only@*/ constraint constraint_makeEnsureLteMaxRead(/*@dependent@*/ /*@observer@*/ exprNode p_index, /*@dependent@*/ /*@observer@*/ exprNode p_buffer);
 
-extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (/*@dependent@*/ /*@oberserver@*/ exprNode p_e, fileloc p_sequencePoint);
+extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (/*@dependent@*/ /*@observer@*/ exprNode p_e, fileloc p_sequencePoint);
 
 extern bool constraint_search (constraint p_c, constraintExpr p_old);
 
@@ -117,7 +117,7 @@ extern bool constraint_same (constraint p_c1, constraint p_c2) ;
 /*@only@*/ cstring  constraint_printOr (constraint p_c) /*@*/;
 extern void constraint_printErrorPostCondition (constraint p_c, fileloc p_loc) ;
 extern constraint constraint_setFcnPre (/*@returned@*/ constraint p_c) ;
-extern constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@oberserver@*/ exprNode p_e) ;
+extern constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@observer@*/ exprNode p_e) ;
 
 extern bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode p_e) ;
 constraint constraint_togglePostOrig (/*@returned@*/ constraint p_c);

diff --git a/src/Headers/constraintExpr.h b/src/Headers/constraintExpr.h
index bc1f609dbaddf12a5e386623fcfc4a0219ab18c9..db9699ed4dc3b358d21f8bbb6177b028cf7222d9 100644 (file)
--- a/src/Headers/constraintExpr.h
+++ b/src/Headers/constraintExpr.h
@@ -71,7 +71,7 @@ bool constraintExpr_search (/*@observer@*/ /*@temp@*/ constraintExpr p_c, /*@obs
 /*@only@*/ fileloc constraintExpr_getFileloc (constraintExpr p_expr);
 
 
-/*@only@*/ constraintExpr constraintExpr_makeSRefMaxset ( /*@temp@*/ /*@oberver@*/ sRef p_s);
+/*@only@*/ constraintExpr constraintExpr_makeSRefMaxset ( /*@temp@*/ /*@observer@*/ sRef p_s);
 
 /*@only@*/ constraintExpr constraintExpr_makeSRefMaxRead(/*@temp@*/ /*@observer@*/ sRef p_s);
 

diff --git a/src/Headers/herald.h b/src/Headers/herald.h
index 36662b4a90c029c6d7646809439b392389b3418f..f929ab5997a7a00c2b986091160005195758d2ea 100644 (file)
--- a/src/Headers/herald.h
+++ b/src/Headers/herald.h
@@ -4,4 +4,4 @@
 /*@constant observer char *LCL_PARSE_VERSION;@*/
 # define LCL_PARSE_VERSION "LCLint 3.0.0.9"
 /*@constant observer char *LCL_COMPILE;@*/
-# define LCL_COMPILE "Compiled using gcc -Wall -g on Linux paisley 2.4.3-12 #1 Fri Jun 8 13:35:30 EDT 2001 i686 unknown by evans"
+# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g -Wall on Linux fowler 2.4.3-12 #1 Fri Jun 8 13:35:30 EDT 2001 i686 unknown by drl7x"

diff --git a/src/Headers/herald.last b/src/Headers/herald.last
index 36662b4a90c029c6d7646809439b392389b3418f..f929ab5997a7a00c2b986091160005195758d2ea 100644 (file)
--- a/src/Headers/herald.last
+++ b/src/Headers/herald.last
@@ -4,4 +4,4 @@
 /*@constant observer char *LCL_PARSE_VERSION;@*/
 # define LCL_PARSE_VERSION "LCLint 3.0.0.9"
 /*@constant observer char *LCL_COMPILE;@*/
-# define LCL_COMPILE "Compiled using gcc -Wall -g on Linux paisley 2.4.3-12 #1 Fri Jun 8 13:35:30 EDT 2001 i686 unknown by evans"
+# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g -Wall on Linux fowler 2.4.3-12 #1 Fri Jun 8 13:35:30 EDT 2001 i686 unknown by drl7x"

diff --git a/src/Headers/local_constants.h b/src/Headers/local_constants.h
index c4c3a887ac645344e32355e5979556d4d408aa9a..73e13fc02ff2ff0ec28919e4f5adc9cc5c4dac80 100644 (file)
--- a/src/Headers/local_constants.h
+++ b/src/Headers/local_constants.h
@@ -2,6 +2,6 @@
 /*@constant observer char *SYSTEM_LIBDIR;@*/
 # define SYSTEM_LIBDIR "/usr/include"
 /*@constant observer char *DEFAULT_LARCHPATH;@*/
-# define DEFAULT_LARCHPATH "/usr/local/lclint-2.5m/lib"
+# define DEFAULT_LARCHPATH ".:/af9/drl7x/re3/LCLintDev/lib"
 /*@constant observer char *DEFAULT_LCLIMPORTDIR;@*/
-# define DEFAULT_LCLIMPORTDIR "/usr/local/lclint-2.5m/imports"
+# define DEFAULT_LCLIMPORTDIR "/af9/drl7x/re3/LCLintDev/imports"

diff --git a/src/Headers/local_constants.last b/src/Headers/local_constants.last
index c4c3a887ac645344e32355e5979556d4d408aa9a..73e13fc02ff2ff0ec28919e4f5adc9cc5c4dac80 100644 (file)
--- a/src/Headers/local_constants.last
+++ b/src/Headers/local_constants.last
@@ -2,6 +2,6 @@
 /*@constant observer char *SYSTEM_LIBDIR;@*/
 # define SYSTEM_LIBDIR "/usr/include"
 /*@constant observer char *DEFAULT_LARCHPATH;@*/
-# define DEFAULT_LARCHPATH "/usr/local/lclint-2.5m/lib"
+# define DEFAULT_LARCHPATH ".:/af9/drl7x/re3/LCLintDev/lib"
 /*@constant observer char *DEFAULT_LCLIMPORTDIR;@*/
-# define DEFAULT_LCLIMPORTDIR "/usr/local/lclint-2.5m/imports"
+# define DEFAULT_LCLIMPORTDIR "/af9/drl7x/re3/LCLintDev/imports"

diff --git a/src/Makefile b/src/Makefile
index 2dd90c04aba805b945a3aeb9b62eed33955a3840..0332ea9334f8b2ffb0449587860e9d0370a45324 100644 (file)
--- a/src/Makefile
+++ b/src/Makefile
@@ -389,7 +389,7 @@ linttest:
        ${LCLINTNEW} -f lclint.lclintrc $(CPPFLAGS) +singleinclude cpphash.c +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -exportlocal -constuse -mts file -mts filerw +partial
 
 lint: 
-       ../bin/lclint -f lclint.lclintrc $(CPPFLAGS) +singleinclude $(ALLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -exportlocal -constuse 
+       ../bin/lclint -f lclint.lclintrc $(CPPFLAGS) +singleinclude $(ALLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -supcounts -fcnuse -exportlocal -constuse 
 
 # -mts file
 

diff --git a/src/Makefile.sources b/src/Makefile.sources
index 0cb998413923df6f0d37b38b3da30ffc25f8c4a9..7281241c753f7f80c86264c0fb51371933716fd4 100644 (file)
--- a/src/Makefile.sources
+++ b/src/Makefile.sources
@@ -27,13 +27,13 @@ GRAMS      = cgrammar.y cscanner.l llgrammar.y signature.y mtgrammar.y
 GRAMSRC    = cgrammar.c cscanner.c mtscanner.c mtreader.c mtgrammar.c
 
 OVERFLOWCHSRC = \
+    constraintGeneration.c \
     constraintTerm.c \
     constraintExprData.c \
     constraintExpr.c \
     constraint.c \
     constraintList.c \
     constraintResolve.c \
-    constraintGeneration.c \
     constraintOutput.c \
     forjunk.c 
     

diff --git a/src/constraint.c b/src/constraint.c
index 84887342818fbc215ff44e3e672d0101939fc429..4f2b8921cb2d625e625bfd4f6e968b500a344df4 100644 (file)
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -309,13 +309,16 @@ static bool checkForMaxSet (constraint c)
 
 bool constraint_hasMaxSet(constraint c)
 {
+  if (checkForMaxSet(c) )
+    return TRUE;
+  
   if (c->orig != NULL)
     {
       if (checkForMaxSet(c->orig) )
        return TRUE;
     }
 
-  return (checkForMaxSet(c) );
+  return FALSE;
 }
 
 constraint constraint_makeReadSafeExprNode (  exprNode po, exprNode ind)
@@ -739,7 +742,10 @@ void constraint_printError (constraint c, fileloc loc)
        }
       else
        {
-         voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
+         if (constraint_hasMaxSet (c) )
+           voptgenerror (FLG_ARRAYBOUNDS, string, errorLoc);
+         else
+           voptgenerror (FLG_ARRAYBOUNDSREAD, string, errorLoc);
        }
       fileloc_free(temp);
       errorLoc = NULL;
@@ -769,6 +775,7 @@ static cstring constraint_printDeep (constraint c)
   
   if (c->orig != constraint_undefined)
     {
+      st = cstring_appendChar(st, '\n');
       genExpr =  exprNode_unparse(c->orig->generatingExpr);
       if (!c->post)
        {
@@ -776,7 +783,7 @@ static cstring constraint_printDeep (constraint c)
            st = cstring_concatFree(st, (message(" derived from %s precondition: %q", genExpr, constraint_printDeep(c->orig) )
                                         ) );
          else
-           st = cstring_concatFree(st,(message(" needed to satisfy %q",
+           st = cstring_concatFree(st,(message(" needed to satisfy precondition:\n%q",
                                                constraint_printDeep(c->orig) )
                                        ) );
          
@@ -823,32 +830,38 @@ static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/
 cstring  constraint_printDetailed (constraint c)
 {
   cstring st = cstring_undefined;
-  cstring genExpr;
+  cstring temp = cstring_undefined;
+    cstring genExpr;
   
   if (!c->post)
     {
-      st = message ("Unresolved constraint:\nLclint is unable to resolve %q", constraint_printDeep (c) );
+      st = message ("Unable to resolve constraint:\n%q", constraint_printDeep (c) );
     }
   else
     {
       st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
     }
 
+  if (constraint_hasMaxSet(c) )
+    {
+      temp = cstring_makeLiteral("Possible out-of-bounds store.  ");
+    }
+  else
+    {
+      temp = cstring_makeLiteral("Possible out-of-bounds read.  ");
+    }
+
+  st  = cstring_concatFree(temp,st);
+  
   genExpr = exprNode_unparse (c->generatingExpr);
 
   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
     {
-      cstring temp;
-      // llassert (c->generatingExpr);
-      temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
-                     genExpr );
+      temp = message ("\nConstraint generated from expression: %s at %q\n",
+                     genExpr,
+                     fileloc_unparse( exprNode_getfileloc (c->generatingExpr) )
+                     );
       st = cstring_concatFree (st, temp);
-
-      if (constraint_hasMaxSet(c) )
-       {
-         temp = message ("Has MaxSet\n");
-         st = cstring_concatFree (st, temp);
-       }
     }
   return st;
 }
@@ -860,11 +873,11 @@ cstring  constraint_printDetailed (constraint c)
   llassert (c !=NULL);
   if (c->post)
     {
-      type = cstring_makeLiteral ("Ensures: ");
+      type = cstring_makeLiteral ("ensures: ");
     }
   else
     {
-      type = cstring_makeLiteral ("Requires: ");
+      type = cstring_makeLiteral ("requires: ");
     }
   st = message ("%q: %q %q %q",
                type,

diff --git a/src/constraintExpr.c b/src/constraintExpr.c
index d747ad6fcb20a0721cf24be86e5267f69a3e53b5..39e416e638b1fdb9d743786e8bda44f1d82b9357 100644 (file)
--- a/src/constraintExpr.c
+++ b/src/constraintExpr.c
@@ -789,13 +789,13 @@ static cstring constraintExprUnaryOpKind_print (constraintExprUnaryOpKind op)
   switch (op)
     {
     case MAXSET:
-      return message("MAXSET");
+      return message("maxSet");
     case MINSET:
-      return message("MINSET");
+      return message("minSet");
     case MAXREAD:
-      return message("MAXREAD");
+      return message("maxRead");
     case MINREAD:
-      return message("MINREAD");
+      return message("minRead");
     default:
       llassert(FALSE);
       return message ("<(Unary OP OTHER>");
@@ -1484,7 +1484,7 @@ bool constraintExpr_hasMaxSet (constraintExpr expr) /*@*/
 
   t = constraintExpr_unparse(expr);
 
-  if (cstring_containsLit(t, "MAXSET") != NULL )
+  if (cstring_containsLit(t, "maxSet") != NULL )
     {
       cstring_free(t);
       return (TRUE);

diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c
index 9e413d35b90a2a16eb1729548fe8db79b51b73bf..5919beebc9b0f91679ce242826b4f915676affb7 100644 (file)
--- a/src/constraintGeneration.c
+++ b/src/constraintGeneration.c
@@ -49,7 +49,7 @@ static  constraintList checkCall (/*@dependent@*/ exprNode p_fcn, exprNodeList p
   */
 //}
 
-static bool exprNode_isUnhandled (/*@dependent@*/ /*@obsever@*/ exprNode e)
+static bool exprNode_isUnhandled (/*@dependent@*/ /*@observer@*/ exprNode e)
 {
   llassert( exprNode_isDefined(e) );
   switch (e->kind)
@@ -182,7 +182,7 @@ if (exprNode_handleError (e) != NULL)
 
 }
 
-static void exprNode_stmt ( /*@dependent@*/ exprNode e)
+static void exprNode_stmt ( /*@dependent@*/ /*@temp@*/ exprNode e)
 {
   exprNode snode;
   fileloc loc;
@@ -560,10 +560,18 @@ static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred,
       
 }
 
-static void exprNode_doGenerateConstraintSwitch ( exprNode switchExpr,
-                                                 exprNode body, constraintList * currentRequires, constraintList *
-                                                 currentEnsures,  constraintList * savedRequires, constraintList *
+static /*@dependent@*/ exprNode exprNode_makeDependent(/*@returned@*/  exprNode e)
+{
+  /*@-temptrans@*/
+  return e;
+  /*@=temptrans@*/  
+}
+
+static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switchExpr,
+                                                 /*@dependent@*/ exprNode body, /*@special@*/ constraintList * currentRequires, /*@special@*/  constraintList *
+                                                 currentEnsures,  /*@special@*/  constraintList * savedRequires, /*@special@*/ constraintList *
                                                  savedEnsures)
+     /*@post:only *currentRequires,  *currentEnsures,  *savedRequires, *savedEnsures @*/ /*@defines *currentRequires,  *currentEnsures,  *savedRequires, *savedEnsures @*/
 {
   exprNode stmt, stmtList;
 
@@ -573,7 +581,14 @@ static void exprNode_doGenerateConstraintSwitch ( exprNode switchExpr,
 
   if (exprNode_isError(body) )
     {
+      *currentRequires = constraintList_makeNew();
+      *currentEnsures = constraintList_makeNew();
+
+      *savedRequires = constraintList_makeNew();
+      *savedEnsures = constraintList_makeNew();
+      /*@-onlytrans@*/
       return;
+      /*@=onlytrans@*/      
     }
 
   if (body->kind != XPR_STMTLIST )
@@ -585,12 +600,16 @@ stmtlist: %s",
       //      llassert(body->kind == XPR_STMT );
       stmt = body;
       stmtList = exprNode_undefined;
+      stmt = exprNode_makeDependent(stmt);
+      stmtList = exprNode_makeDependent(stmtList);
+    }
+  else
+    {
+      stmt     = exprData_getPairB(body->edata);
+      stmtList = exprData_getPairA(body->edata);
+      stmt = exprNode_makeDependent(stmt);
+      stmtList = exprNode_makeDependent(stmtList);
     }
-    else
-      {
-       stmt     = exprData_getPairB(body->edata);
-       stmtList = exprData_getPairA(body->edata);
-      }
 
   DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s
 stmt: %s",
@@ -602,9 +621,14 @@ stmt: %s",
                                       savedRequires, savedEnsures );
 
   if (exprNode_isError(stmt) )
+    /*@-onlytrans@*/
     return;
+    /*@=onlytrans@*/
 
   exprNode_stmt(stmt);
+
+  switchExpr = exprNode_makeDependent (switchExpr);
+    
   //, FALSE, FALSE, exprNode_getfileloc(stmt) );
 
   if (! exprNode_isCaseMarker(stmt) )
@@ -618,9 +642,9 @@ stmt: %s",
       temp = constraintList_reflectChanges (stmt->requiresConstraints,
                                            *currentEnsures);
 
-            *currentRequires = constraintList_mergeRequiresFreeFirst
-             (*currentRequires,
-              temp);
+            *currentRequires = constraintList_mergeRequiresFreeFirst(
+                                                                    *currentRequires,
+                                                                    temp);
 
            constraintList_free(temp);
 
@@ -632,7 +656,10 @@ stmt: %s",
                                    exprNode_unparse(switchExpr), exprNode_unparse(body),
                                    constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
                                    ) ));
+                 /*@-onlytrans@*/
                  return;
+                 /*@=onlytrans@*/
+
     }
 
   if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList) )
@@ -648,19 +675,21 @@ stmt: %s",
       if (constraintList_isUndefined(*savedEnsures) &&
          constraintList_isUndefined(*savedRequires) )
        {
+         llassert(constraintList_isUndefined(*savedEnsures) );
+         llassert(constraintList_isUndefined(*savedRequires) );
          *savedEnsures  = constraintList_copy(*currentEnsures);
          *savedRequires = constraintList_copy(*currentRequires);
        }
-             else
-              {
-                DPRINTF (( message("Doing logical or") ));
-                temp = constraintList_logicalOr (*savedEnsures, *currentEnsures);
-                constraintList_free (*savedEnsures);
-                *savedEnsures = temp;
-
-                *savedRequires = constraintList_mergeRequiresFreeFirst (*savedRequires, *currentRequires);
-              }
-
+      else
+       {
+         DPRINTF (( message("Doing logical or") ));
+         temp = constraintList_logicalOr (*savedEnsures, *currentEnsures);
+         constraintList_free (*savedEnsures);
+         *savedEnsures = temp;
+         
+         *savedRequires = constraintList_mergeRequiresFreeFirst (*savedRequires, *currentRequires);
+       }
+      
       con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
                                        (stmt->edata), exprNode_getfileloc(stmt) );
 
@@ -703,29 +732,40 @@ stmt: %s",
       if (exprNode_isError(stmtList) )
        {
          constraintList_free(*currentEnsures);
-         *currentEnsures = constraintList_copy(ensuresTemp);
-       }
-            else
-             {
 
-               temp = constraintList_logicalOr (*currentEnsures, ensuresTemp);
+         *currentEnsures = constraintList_copy(ensuresTemp);
+         constraintList_free(ensuresTemp);
 
-               constraintList_free(*currentEnsures);
-               constraintList_free(ensuresTemp);
+       }
+      else
+       {
+         
+         temp = constraintList_logicalOr (*currentEnsures, ensuresTemp);
+         
+         constraintList_free(*currentEnsures);
+         constraintList_free(ensuresTemp);
 
-               *currentEnsures = temp;
-             }
+         *currentEnsures = temp;
+       }
       constraintList_free(*currentRequires);
-
+      
       *currentRequires = constraintList_makeNew();
     }
+  else
+    {
+      // we handle the case of ! exprNode_isCaseMarker above
+      // the else if clause should always be true.
+      BADEXIT;
+    }
 
   DPRINTF(( message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
                    "%s currentEnsures:%s",
                    exprNode_unparse(switchExpr), exprNode_unparse(body),
                    constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
                    ) ));
+  /*@-onlytrans@*/ 
   return;
+  /*@=onlytrans@*/ 
 
 }
 
@@ -747,12 +787,13 @@ static void exprNode_generateConstraintSwitch ( exprNode switchStmt)
   if ( body->kind == XPR_BLOCK)
     body = exprData_getSingle(body->edata);
 
+  /*
   constraintsRequires = constraintList_undefined;
   constraintsEnsures = constraintList_undefined;
 
   lastRequires = constraintList_makeNew();
   lastEnsures = constraintList_makeNew();
-
+  */
 
   exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires, &lastEnsures, &constraintsRequires, &constraintsEnsures);
 
@@ -769,11 +810,11 @@ static void exprNode_generateConstraintSwitch ( exprNode switchStmt)
       constraintList_free (constraintsRequires);
       constraintList_free (constraintsEnsures);
     }
-    else
-      {
-       switchStmt->ensuresConstraints =    constraintList_copy(lastEnsures);
-       switchStmt->requiresConstraints =   constraintList_copy(lastRequires);
-      }
+  else
+    {
+      switchStmt->ensuresConstraints =    constraintList_copy(lastEnsures);
+      switchStmt->requiresConstraints =   constraintList_copy(lastRequires);
+    }
 
   constraintList_free (lastRequires);
   constraintList_free (lastEnsures);

diff --git a/src/constraintList.c b/src/constraintList.c
index c9fe9a50719f1b0c7551a401687bad5e7bb3ec1f..4fcf3a3e78e69fa24130efde92df39a04b3e915c 100644 (file)
--- a/src/constraintList.c
+++ b/src/constraintList.c
@@ -51,7 +51,7 @@
 # define end_constraintList_elements_private }}}
 
 
-constraintList constraintList_makeNew ()
+/*@only@*/ constraintList constraintList_makeNew ()
 {
   constraintList s = (constraintList) dmalloc (sizeof (*s));
 
@@ -360,7 +360,7 @@ constraintList_free (/*@only@*/ constraintList s)
 }
 
 constraintList
-constraintList_copy (/*@oberserver@*/ /*@temp@*/ constraintList s)
+constraintList_copy (/*@observer@*/ /*@temp@*/ constraintList s)
 {
   constraintList ret = constraintList_makeNew ();
 
@@ -384,7 +384,7 @@ constraintList constraintList_preserveOrig (constraintList c)
   return c;
 }
 
-constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@depenent@*/ /*@observer@*/  exprNode fcn)
+constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@dependent@*/ /*@observer@*/  exprNode fcn)
 {
   DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
 

diff --git a/src/constraintTerm.c b/src/constraintTerm.c
index 6f88df006c5f34d57c44d755ef0b70d1a58b213d..288d6db0d27807ba4d8f106576bb8d3799f11a0f 100644 (file)
--- a/src/constraintTerm.c
+++ b/src/constraintTerm.c
@@ -132,7 +132,7 @@ constraintTermType constraintTerm_getKind (constraintTerm t)
   return (t->value.sref);
 }
 
-/*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@depenedent@*/  exprNode e)
+/*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@dependent@*/  exprNode e)
 {
   constraintTerm ret = new_constraintTermExpr();
   ret->loc =  fileloc_copy(exprNode_getfileloc(e));

diff --git a/src/exprChecks.c b/src/exprChecks.c
index e662771e5c7d4aacf0011e56068b28436a392ed1..3691147717d243754668ec08c8c136ca55a92d78 100644 (file)
--- a/src/exprChecks.c
+++ b/src/exprChecks.c
@@ -938,6 +938,8 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode fcnBody
     // check if errors will printed
     if (! (context_getFlag(FLG_DEBUGFUNCTIONCONSTRAINT) ||
           context_getFlag(FLG_FUNCTIONCONSTRAINT) ||
+          context_getFlag(FLG_ARRAYBOUNDS) ||
+          context_getFlag(FLG_ARRAYBOUNDSREAD) ||
           context_getFlag(FLG_CHECKPOST) 
           )
        )

diff --git a/src/flags.def b/src/flags.def
index e9626b939471b755ee8eb0677a51e5c259bc7e95..46abe44c047d7bfa470550774fba80a6ff49618d 100644 (file)
--- a/src/flags.def
+++ b/src/flags.def
@@ -2818,6 +2818,24 @@ static flaglist flags =
     "This flag is for debuging.  It causes lclint to perform buffer overflow checking even if the error will be surpressed.  Normal buffer overflow checking will only be performed if errors would be printed. ",
     0, 0
   },
+  
+  {
+    FK_NT, FK_MEMORY, modeFlag,
+    "arrayBounds",
+    FLG_ARRAYBOUNDS,
+    "Possible out-of-bounds store.  Unable to resolve 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
+  },
+  {
+    FK_NT, FK_MEMORY, modeFlag,
+    "arrayBoundsRead",
+    FLG_ARRAYBOUNDSREAD,
+    "Possible out-of-bounds read.  Unable to resolve 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
+  },
+
   {
     FK_NT, FK_MEMORY, modeFlag,
     "fcnconstraint",

diff --git a/src/llmain.c b/src/llmain.c
index 08296486197d6b6023490eddf2b56d5be2d02d86..8210121cec889f477047686166d4ed77ce6e0f8e 100644 (file)
--- a/src/llmain.c
+++ b/src/llmain.c
@@ -94,7 +94,7 @@ static void showHelp (void);
 static void interrupt (int p_i);
 
 static void loadrc (/*@open@*/ FILE *p_rcfile, cstringSList *p_passThroughArgs)
-   /*@ensures closed p_rcfile@*/ ;
+     ; // /*@ensures closed p_rcfile@*/ ;
 
 static void describeVars (void);
 static bool specialFlagsHelp (char *p_next);
@@ -2146,7 +2146,7 @@ llexit (int status)
 
 void
 loadrc (/*@open@*/ FILE *rcfile, cstringSList *passThroughArgs)
-    /*@ensures closed rcfile@*/
+     //    /*@ensures closed rcfile@*/
 {
   char *s = mstring_create (MAX_LINE_LENGTH);
   char *os = s;

diff --git a/test/Makefile b/test/Makefile
index 6d0849b7552d6d73bdfdc95e98c22cdddc7ca2ec..6bcd22d84e90b23610a7d716b010969e1f6f3944 100644 (file)
--- a/test/Makefile
+++ b/test/Makefile
@@ -421,7 +421,7 @@ mongoincludes:
        $(LCLINTR) mongoincludes.c -includenest 5 -expect 0
 
 mystrncat:
-       $(LCLINTR) mystrncat.c +fcnconstraint -expect 4 
+       $(LCLINTR) mystrncat.c +arrayBounds +arrayBoundsRead -expect 4 
 
 noeffect:
        ${LCLINT} noeffect.c +allmacros +checks -expect 3
@@ -651,19 +651,19 @@ tests2.4:
 
 sizeoftest:
        @cd sizeoftest; \
-       $(LCLINTR) +functionconstraint sizeof.c
+       $(LCLINTR) +arrayBounds +arrayBoundsRead sizeof.c
 
 bufferTest:
        @cd bufferTest; \
-       $(LCLINTR) +functionconstraint test4.c test6.c
+       $(LCLINTR) +arrayBounds +arrayBoundsRead test4.c test6.c
 
 simplebufferConstraintTests:
        @cd simplebufferConstraintTests; \
-       $(LCLINTR) +functionconstraint m.c  sizeof.c  test3.c  test7.c
+       $(LCLINTR) +arrayBounds +arrayBoundsRead m.c  sizeof.c  test3.c  test7.c
 
 moreBufferTests:
        @cd moreBufferTests; \
-       $(LCLINTR) +functionconstraint +orconstraint unrecogCall.c strrchr.c initialization.c simplifyTest.c strncatNotReallyGood.c strncatReallyGood.c
+       $(LCLINTR) +arrayBounds +arrayBoundsRead +orconstraint unrecogCall.c strrchr.c initialization.c simplifyTest.c strncatNotReallyGood.c strncatReallyGood.c
 
 maxset:
        @cd maxset; \
@@ -673,16 +673,15 @@ maxset:
 
 globalbufferannotation:
        @cd globalbufferannotation; \
-       $(LCLINTR) +functionconstraint globalvariable.c
-
+       $(LCLINTR) +arrayBounds +arrayBoundsRead globalvariable.c
 
 strchr:
        @cd strchr; \
-       $(LCLINTR) -f .lclintrc -booltype "lltX_bool" strchr.c
+       $(LCLINTR)  +arrayBounds +arrayBoundsRead  strchr.c
 
 for:
        @cd for; \
-       $(LCLINTR) -f .lclintrc -booltype "lltX_bool" for.c
+       $(LCLINTR)  +arrayBounds +arrayBoundsRead  for.c
 
 tests2.5:
        setenv LCLINT '$(LCLINTRN)'; cd tests2.5 ; $(MAKE) -e

diff --git a/test/abst_t.lcs b/test/abst_t.lcs
index c4550e30657c808fa6c89095bbed22e862b5a832..ced8c30ce07f23f6ddedf2f6e650e89d6df35744 100644 (file)
--- a/test/abst_t.lcs
+++ b/test/abst_t.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/abstptr.lcs b/test/abstptr.lcs
index 844ef60721d3d22230adb91bb1b05772c1f3ca14..0d4f79bbb0b7efc6a1ea70cf505717550ed1dc5f 100644 (file)
--- a/test/abstptr.lcs
+++ b/test/abstptr.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/alias.lcs b/test/alias.lcs
index 31f1965b4f55c2793599af4f7a57e5c88a6329cf..d1f6aba3d26c9de2f7cc3ecfaaef275ce17d1298 100644 (file)
--- a/test/alias.lcs
+++ b/test/alias.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/alias2.lcs b/test/alias2.lcs
index 936f48e8609dfe2eb1692c72232cb4c8fbad36e6..3ddc4e534604aae70312ef56cdf9390b4dc8ea81 100644 (file)
--- a/test/alias2.lcs
+++ b/test/alias2.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/alias3.lcs b/test/alias3.lcs
index 6eaf76140709c0f2d39fa3b6f484115fd9a8dcd8..da7944a4f840206701337ca7e0345fcf72937e1d 100644 (file)
--- a/test/alias3.lcs
+++ b/test/alias3.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/alias3.lh b/test/alias3.lh
index 3e4e9899c27e09c6e028eadcde3ccc20318c9930..83dec3937a88f7f350b2aacfb9bdad4bdc9785be 100644 (file)
--- a/test/alias3.lh
+++ b/test/alias3.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 # include "bool.h"
 
 

diff --git a/test/alias4.lcs b/test/alias4.lcs
index e14f7f0794692743e438f62a8b66f54c5c6cbc8a..9041d55e6a87b7de0ec8086e2b02571ae56961ee 100644 (file)
--- a/test/alias4.lcs
+++ b/test/alias4.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/alias4.lh b/test/alias4.lh
index 8a2391c13f4e950d6455dc432db654cce61889d5..9713c6808f6dd8d627067bf0168034c07f027023 100644 (file)
--- a/test/alias4.lh
+++ b/test/alias4.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "mut.h"

diff --git a/test/alias5.lcs b/test/alias5.lcs
index a3f265e55048bf3f5c47a09ed1cb2fb69b92d4b2..ac0ef5d3af461c8f026b818738495fce7d6c95f6 100644 (file)
--- a/test/alias5.lcs
+++ b/test/alias5.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/alias5.lh b/test/alias5.lh
index 87c840b1d1451c8b5458a7ba59ded25e3e3bfb26..1151b4c45318dd5cb9cb09c83dda0d59dd227dfa 100644 (file)
--- a/test/alias5.lh
+++ b/test/alias5.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 # include "bool.h"
 
 

diff --git a/test/argorder2.lcs b/test/argorder2.lcs
index de443606fc53f8d9e9d10f9843acee2b8dd88d2a..664e3cedbdf66169f51def46329979a059594fb3 100644 (file)
--- a/test/argorder2.lcs
+++ b/test/argorder2.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/argorder4.lcs b/test/argorder4.lcs
index 7313739f72af2a5e2d6c7988becf62b37226b44b..7b28e8336a3dbcd78d67e62a6007b62cff934cb7 100644 (file)
--- a/test/argorder4.lcs
+++ b/test/argorder4.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/args.lcs b/test/args.lcs
index 35c3d687fd79790f23169504c4f7895e1672ad80..57ed249a0aa2de7f1e131592c96eb4b5a71d82ea 100644 (file)
--- a/test/args.lcs
+++ b/test/args.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/bufferTest.expect b/test/bufferTest.expect
index 4aeb1c36829d40b97a4580025185acd9d96e702e..4d59c0eca8c177cfb6bbb9a90eb963bf9d112774 100644 (file)
--- a/test/bufferTest.expect
+++ b/test/bufferTest.expect
@@ -1,20 +1,21 @@
 
 test4.c: (in function t)
 test4.c:6:3: Variable g used before definition
-test4.c:6:3: Unresolved constraint:
-    Lclint is unable to resolve Requires: : MAXSET ((g @ test4.c:6:3 ) )  >=  (
-    100 )  needed to satisfy Requires: : MAXSET ((g @ test4.c:6:3 ) )  >=  (
-    100 ) 
+test4.c:6:3: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : maxSet ((g @ test4.c:6:3 ) )  >=  ( 100 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((g @ test4.c:6:3 ) )  >=  ( 100 ) 
 test6.c:2:6: Function t defined more than once
    test4.c:15:1: Previous definition of t
 test6.c: (in function t)
 test6.c:5:4: Variable g used before definition
-test6.c:6:3: Unresolved constraint:
-    Lclint is unable to resolve Requires: : MAXSET ((g @ test6.c:5:4 ) )  >=  (
-    1 )  needed to satisfy Requires: : MAXSET ((g @ test6.c:6:3 ) )  >=  ( 0 ) 
-test6.c:6:10: Unresolved constraint:
-    Lclint is unable to resolve Requires: : MAXREAD ((g @ test6.c:5:4 ) )  >= 
-    ( 2 )  needed to satisfy Requires: : MAXREAD ((g @ test6.c:6:10 ) )  >=  (
-    1 ) 
+test6.c:6:3: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : maxSet ((g @ test6.c:5:4 ) )  >=  ( 1 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((g @ test6.c:6:3 ) )  >=  ( 0 ) 
+test6.c:6:10: Possible out-of-bounds read.  Unable to resolve constraint:
+    requires: : maxRead ((g @ test6.c:5:4 ) )  >=  ( 2 ) 
+     needed to satisfy precondition:
+    requires: : maxRead ((g @ test6.c:6:10 ) )  >=  ( 1 ) 
 
 Finished LCLint checking --- 6 code errors found

diff --git a/test/bufferTest.out b/test/bufferTest.out
index 4aeb1c36829d40b97a4580025185acd9d96e702e..4d59c0eca8c177cfb6bbb9a90eb963bf9d112774 100644 (file)
--- a/test/bufferTest.out
+++ b/test/bufferTest.out
@@ -1,20 +1,21 @@
 
 test4.c: (in function t)
 test4.c:6:3: Variable g used before definition
-test4.c:6:3: Unresolved constraint:
-    Lclint is unable to resolve Requires: : MAXSET ((g @ test4.c:6:3 ) )  >=  (
-    100 )  needed to satisfy Requires: : MAXSET ((g @ test4.c:6:3 ) )  >=  (
-    100 ) 
+test4.c:6:3: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : maxSet ((g @ test4.c:6:3 ) )  >=  ( 100 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((g @ test4.c:6:3 ) )  >=  ( 100 ) 
 test6.c:2:6: Function t defined more than once
    test4.c:15:1: Previous definition of t
 test6.c: (in function t)
 test6.c:5:4: Variable g used before definition
-test6.c:6:3: Unresolved constraint:
-    Lclint is unable to resolve Requires: : MAXSET ((g @ test6.c:5:4 ) )  >=  (
-    1 )  needed to satisfy Requires: : MAXSET ((g @ test6.c:6:3 ) )  >=  ( 0 ) 
-test6.c:6:10: Unresolved constraint:
-    Lclint is unable to resolve Requires: : MAXREAD ((g @ test6.c:5:4 ) )  >= 
-    ( 2 )  needed to satisfy Requires: : MAXREAD ((g @ test6.c:6:10 ) )  >=  (
-    1 ) 
+test6.c:6:3: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : maxSet ((g @ test6.c:5:4 ) )  >=  ( 1 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((g @ test6.c:6:3 ) )  >=  ( 0 ) 
+test6.c:6:10: Possible out-of-bounds read.  Unable to resolve constraint:
+    requires: : maxRead ((g @ test6.c:5:4 ) )  >=  ( 2 ) 
+     needed to satisfy precondition:
+    requires: : maxRead ((g @ test6.c:6:10 ) )  >=  ( 1 ) 
 
 Finished LCLint checking --- 6 code errors found

diff --git a/test/cast.lcs b/test/cast.lcs
index 8555fb8b73cc68e477936d1b7055fcafa9ecb237..3bd3a143148a3cf9d229bf3f62c59dc4180ea53c 100644 (file)
--- a/test/cast.lcs
+++ b/test/cast.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db1/bool.lcs b/test/db1/bool.lcs
index 2cac936f7ae9fa018b31992f64c8257f287dc9e9..a6ab36082ffb08c6636740f40fa695d75c1e1aeb 100644 (file)
--- a/test/db1/bool.lcs
+++ b/test/db1/bool.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db1/bool.lh b/test/db1/bool.lh
index 3b2810c4ac1da5e781e91c9572262a1a8cd82fce..5458a3bbe19b64c2cd72310b17b50e407ac988ed 100644 (file)
--- a/test/db1/bool.lh
+++ b/test/db1/bool.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 # include "bool.h"
 
 

diff --git a/test/db1/dbase.lcs b/test/db1/dbase.lcs
index 041e4d594eb75fde76af1cb49423428b7df305b2..2990998b7bf6555fdec4a1ea1218be5bf1048a5f 100644 (file)
--- a/test/db1/dbase.lcs
+++ b/test/db1/dbase.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db1/dbase.lh b/test/db1/dbase.lh
index 255594850fa172a05b202d3653b982cda1675e7f..919a715049ca4540cddb194a1283064ac17c8cca 100644 (file)
--- a/test/db1/dbase.lh
+++ b/test/db1/dbase.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include <stdio.h>
 # include "bool.h"

diff --git a/test/db1/employee.lcs b/test/db1/employee.lcs
index b3571e47e025e276cfededc5297e60e3c8458533..dd6cff4cb29f4328ee775caa87f9e8ee16ffbeaa 100644 (file)
--- a/test/db1/employee.lcs
+++ b/test/db1/employee.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db1/employee.lh b/test/db1/employee.lh
index 934a3dc881b1217e32a0f63624add872422c7f39..f56b083bb02d37365a83a167f0692da6e22178c9 100644 (file)
--- a/test/db1/employee.lh
+++ b/test/db1/employee.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "bool.h"

diff --git a/test/db1/empset.lcs b/test/db1/empset.lcs
index 8701555a4fb3b245ae18a7210dc85017e5622a87..d06e7ead1d85bbbf33d581273c8270ccf58fa6f0 100644 (file)
--- a/test/db1/empset.lcs
+++ b/test/db1/empset.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db1/empset.lh b/test/db1/empset.lh
index 5655774072dc1a474389fb16988858be2905b93d..1de89d5ffd8437f853ddeb0ebc7db0a69e799659 100644 (file)
--- a/test/db1/empset.lh
+++ b/test/db1/empset.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "employee.h"

diff --git a/test/db1/erc.lcs b/test/db1/erc.lcs
index 525dc5da9f18731ab56827b1b51159a6cda2411b..a57e1c2b08b22d6414c4f5744bde307572d041fb 100644 (file)
--- a/test/db1/erc.lcs
+++ b/test/db1/erc.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db1/erc.lh b/test/db1/erc.lh
index 53e2fdf5f30709eea0ad66bfa677def8f8a9816c..40c9beab34f956946ad19077cf8322290ccef517 100644 (file)
--- a/test/db1/erc.lh
+++ b/test/db1/erc.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "eref.h"

diff --git a/test/db1/eref.lcs b/test/db1/eref.lcs
index c310e47b70bc5a14331abb6c8b934b2732fe5962..e2ba30042c01035e80be17f6df2cacca2d64ea38 100644 (file)
--- a/test/db1/eref.lcs
+++ b/test/db1/eref.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db1/eref.lh b/test/db1/eref.lh
index b3aa26a001d9efd5af2fcd7ccd009d7c6c116e7f..30c9423fa890a15b99e5823ca5bf8b303166d85e 100644 (file)
--- a/test/db1/eref.lh
+++ b/test/db1/eref.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "employee.h"

diff --git a/test/db1/ereftab.lcs b/test/db1/ereftab.lcs
index 6cbd720aa2b79632d638f4a6226751733082bcb8..dafa742a6ab5e5009041b7423d7a7fce9538dcab 100644 (file)
--- a/test/db1/ereftab.lcs
+++ b/test/db1/ereftab.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db1/ereftab.lh b/test/db1/ereftab.lh
index b5889f80f5bb09d4c615337b17cbca550fc281fc..e12eb357307ae650695511e4fe5523b02bc51900 100644 (file)
--- a/test/db1/ereftab.lh
+++ b/test/db1/ereftab.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "employee.h"

diff --git a/test/db2/dbase.lcs b/test/db2/dbase.lcs
index 8a906ce8defdc2d8306a0a1ba74d29b63d38ea69..fdac799502788135354642a2caac4c3e7550f6b3 100644 (file)
--- a/test/db2/dbase.lcs
+++ b/test/db2/dbase.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db2/dbase.lh b/test/db2/dbase.lh
index 255594850fa172a05b202d3653b982cda1675e7f..919a715049ca4540cddb194a1283064ac17c8cca 100644 (file)
--- a/test/db2/dbase.lh
+++ b/test/db2/dbase.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include <stdio.h>
 # include "bool.h"

diff --git a/test/db2/employee.lcs b/test/db2/employee.lcs
index 02300ee1be98805826591142f38cc14f44aa7cc8..ef85848fe9e25dfb59c10e7d3e1a14d142d44925 100644 (file)
--- a/test/db2/employee.lcs
+++ b/test/db2/employee.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db2/employee.lh b/test/db2/employee.lh
index 0ca4bc23ce6ca7d4de9f96795d44ade2468f6c27..8788f0789d1f1705d9a08bbade99fed5a71a07bf 100644 (file)
--- a/test/db2/employee.lh
+++ b/test/db2/employee.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include <stdio.h>
 # include "bool.h"

diff --git a/test/db2/empset.lcs b/test/db2/empset.lcs
index 4a5dcd01aad0bbcb77404fcede541dc725355fa0..775b5b0b81c1823f34832f03e57ed6eec3629911 100644 (file)
--- a/test/db2/empset.lcs
+++ b/test/db2/empset.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db2/empset.lh b/test/db2/empset.lh
index d1a9885a9c8bbbd50cc295f826f5db462d07486c..48c106557f07beb9c1a5449524c95d6055482105 100644 (file)
--- a/test/db2/empset.lh
+++ b/test/db2/empset.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "employee.h"

diff --git a/test/db2/erc.lcs b/test/db2/erc.lcs
index 9390c5c73f124810bc78a682078090673c1693c6..aa70daf7e440259fc56c02d20ba4372d94e81d0d 100644 (file)
--- a/test/db2/erc.lcs
+++ b/test/db2/erc.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db2/erc.lh b/test/db2/erc.lh
index 87aa6d554ca9aee7ef20a788e43e32b6ac7ce8e7..b263cc0266b2a1a2f78c785aa00e67a4e0e3a52d 100644 (file)
--- a/test/db2/erc.lh
+++ b/test/db2/erc.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "eref.h"

diff --git a/test/db2/eref.lcs b/test/db2/eref.lcs
index 8397afd8b83d997d450caf590acb03857b515947..4ade37f9d69404cb513b9c990c89123ac323913f 100644 (file)
--- a/test/db2/eref.lcs
+++ b/test/db2/eref.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db2/eref.lh b/test/db2/eref.lh
index b3aa26a001d9efd5af2fcd7ccd009d7c6c116e7f..30c9423fa890a15b99e5823ca5bf8b303166d85e 100644 (file)
--- a/test/db2/eref.lh
+++ b/test/db2/eref.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "employee.h"

diff --git a/test/db2/ereftab.lcs b/test/db2/ereftab.lcs
index 47ca5c444d4c7f86f931a90c3672539815f30eb4..f944c064cf075761e21edd010fa32812f838e303 100644 (file)
--- a/test/db2/ereftab.lcs
+++ b/test/db2/ereftab.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db2/ereftab.lh b/test/db2/ereftab.lh
index b5889f80f5bb09d4c615337b17cbca550fc281fc..e12eb357307ae650695511e4fe5523b02bc51900 100644 (file)
--- a/test/db2/ereftab.lh
+++ b/test/db2/ereftab.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "employee.h"

diff --git a/test/db3/bool.lcs b/test/db3/bool.lcs
index 2cf18997e332dc63715932f1682b15611410905f..03d71977168cb4184440ba666fc394c76cd5aa7b 100644 (file)
--- a/test/db3/bool.lcs
+++ b/test/db3/bool.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db3/bool.lh b/test/db3/bool.lh
index 379f7ead8e1803ce344e149df10ad7ea2d2d59f9..655b92c7c7ca9e64e3a5670bfb80c2133a57a8f3 100644 (file)
--- a/test/db3/bool.lh
+++ b/test/db3/bool.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 # include "bool.h"
 
 

diff --git a/test/db3/check.lcs b/test/db3/check.lcs
index 90ee3bc74cd30c2e44aa48f3577abd9e8bc9bc82..cf1cf5d8d7247e78c98a9cb7ae5066846f34dfbd 100644 (file)
--- a/test/db3/check.lcs
+++ b/test/db3/check.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db3/check.lh b/test/db3/check.lh
index c78371f5176c0befbed6d06643fc7f160df7a0ad..3e770d10821e82716dba0e7a7718cd653b1fbbf1 100644 (file)
--- a/test/db3/check.lh
+++ b/test/db3/check.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "bool.h"

diff --git a/test/db3/dbase.lcs b/test/db3/dbase.lcs
index af4bc6270657aa69720a679e00e87abb134a415e..4c4145ae586fcfc9b2d9851d5aefec13a2fcd585 100644 (file)
--- a/test/db3/dbase.lcs
+++ b/test/db3/dbase.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db3/dbase.lh b/test/db3/dbase.lh
index fe66110cc1f90938cf18ca4966aeec00398ed661..3d2c92357dfae8dbe8a33bb678713ece264178a5 100644 (file)
--- a/test/db3/dbase.lh
+++ b/test/db3/dbase.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include <stdio.h>
 # include "bool.h"

diff --git a/test/db3/employee.lcs b/test/db3/employee.lcs
index b25b66a6669beaa5cd8918f12b24a42c0c0b0075..0975a16432e4714b303a9bc093636ed513f04662 100644 (file)
--- a/test/db3/employee.lcs
+++ b/test/db3/employee.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db3/employee.lh b/test/db3/employee.lh
index c5d5aae7a07dce864e8ee1e30f66b8d421921e08..a9bc2124404670d73ca0b796bc62e9c96b500ab8 100644 (file)
--- a/test/db3/employee.lh
+++ b/test/db3/employee.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include <stdio.h>
 # include "bool.h"

diff --git a/test/db3/empset.lcs b/test/db3/empset.lcs
index cad11a6f7f2bbd69713f795c65b3da75a9c84b15..4ffcf0f55a68f80f5850714e134e2e3264636dc8 100644 (file)
--- a/test/db3/empset.lcs
+++ b/test/db3/empset.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db3/empset.lh b/test/db3/empset.lh
index 81ae002df76fab478e728e364c8fbd6e06a51c1d..192cc1709d75316118217a99b93b4e5509aa712e 100644 (file)
--- a/test/db3/empset.lh
+++ b/test/db3/empset.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "employee.h"

diff --git a/test/db3/erc.lcs b/test/db3/erc.lcs
index 56c48a2b47ca3351d904cefb1799e9db51b96738..fc22bb3fc942a7f1976f41344a805da1ea0e34c9 100644 (file)
--- a/test/db3/erc.lcs
+++ b/test/db3/erc.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db3/erc.lh b/test/db3/erc.lh
index 978d8a16981044c8529a7104851ea89e888f2c85..b22797cdc10a696a4bf1c97a53f896f4f842667a 100644 (file)
--- a/test/db3/erc.lh
+++ b/test/db3/erc.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "eref.h"

diff --git a/test/db3/eref.lcs b/test/db3/eref.lcs
index 08a90696151ba495a3faa56300067889e79e170f..c0da6f70812bc55fe37773ef609049b3141ebe3f 100644 (file)
--- a/test/db3/eref.lcs
+++ b/test/db3/eref.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db3/eref.lh b/test/db3/eref.lh
index 3af65f60cdb94546d4d8122956122e64a4235761..0e8fbe80fba9460e392bcbe2dd13785372feae84 100644 (file)
--- a/test/db3/eref.lh
+++ b/test/db3/eref.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "employee.h"

diff --git a/test/db3/ereftab.lcs b/test/db3/ereftab.lcs
index 5944bb760f417296037eda97d072166730b741dc..8b731a8d3a220c3cdc5d0d51db07805c004a3a51 100644 (file)
--- a/test/db3/ereftab.lcs
+++ b/test/db3/ereftab.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/db3/ereftab.lh b/test/db3/ereftab.lh
index 4723bf92735d01f3a62faa74f773b1555683e874..b2c5ad12b1ee7484b0a16d99537b1c55f2b81e84 100644 (file)
--- a/test/db3/ereftab.lh
+++ b/test/db3/ereftab.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 
 # include "bool.h"
 # include "employee.h"

diff --git a/test/decl2.lcs b/test/decl2.lcs
index 66f7ce4133243b345e1155b865a2798c53560fd3..62db37a19f776c5296a92ef925cea230d58c056d 100644 (file)
--- a/test/decl2.lcs
+++ b/test/decl2.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/enum.lcs b/test/enum.lcs
index a7ed2183bdb924f12f436c95a3fea20f362e8f51..0a4603f167a188e4617b2a9325d8cfde76f2f2d0 100644 (file)
--- a/test/enum.lcs
+++ b/test/enum.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/for.expect b/test/for.expect
index 22aa76a407a05f98386437f0eb64d3f513962340..6209bae1cd1bbb39f56c9e3f61deaf1087a89110 100644 (file)
--- a/test/for.expect
+++ b/test/for.expect
@@ -1,8 +1,8 @@
 
 for.c: (in function f)
-for.c:13:5: Unresolved constraint:
-    Lclint is unable to resolve Requires: : (i @ for.c:13:7 )   <=  ( 10 ) 
-    needed to satisfy Requires: : MAXSET ((t @ for.c:13:5 ) )  >=  (i @
-    for.c:13:7 ) 
+for.c:13:5: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : (i @ for.c:13:7 )   <=  ( 10 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((t @ for.c:13:5 ) )  >=  (i @ for.c:13:7 ) 
 
 Finished LCLint checking --- 1 code error found

diff --git a/test/for/.lclintrc b/test/for/.lclintrc
index dd00d2e30af92f0680bbda4424b11fd328e69c86..84b3644c58df05f47aa07cc9eebb30b0aa317e8e 100644 (file)
--- a/test/for/.lclintrc
+++ b/test/for/.lclintrc
@@ -1 +1 @@
-+fcnconstraint
++arrayBounds

diff --git a/test/glob.lcs b/test/glob.lcs
index c04b17d0916c2ee98d930e93ddf66a6cb855acf7..2ee1d2d8bb906d505689e509113c20c134262792 100644 (file)
--- a/test/glob.lcs
+++ b/test/glob.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/impabstract.lcs b/test/impabstract.lcs
index e553a351dc1c9d60eb0ff679c8ab240d2e81f48e..94581be5523e7be731ca13f30599740cd5cd0e2a 100644 (file)
--- a/test/impabstract.lcs
+++ b/test/impabstract.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/iter.lcs b/test/iter.lcs
index c3ca7a68fa2b7ae46fe03f7a25a8c8dfcd81dd05..031203f3b7db8b7e03e5dc396c09586d532756f4 100644 (file)
--- a/test/iter.lcs
+++ b/test/iter.lcs
@@ -1,4 +1,4 @@
-%FAILED Output from LCLint 3.0.0.8
+%FAILED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/macros.lcs b/test/macros.lcs
index ac9b85441ffdf41c7072746aa7551564c5e9cd7f..df02aab7fe5cf2c5fa7791556870ff67269251ff 100644 (file)
--- a/test/macros.lcs
+++ b/test/macros.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/macrosef.lcs b/test/macrosef.lcs
index cabe5638e94376802ba8bf0ce0a709a2eee46eb8..d207294242c7130d9840e53b968df38515caccd3 100644 (file)
--- a/test/macrosef.lcs
+++ b/test/macrosef.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/maxset.expect b/test/maxset.expect
index 3973259d14a632869a8df579c9c0106f7ae094e8..9e473f1102a254212fdbe66d80e67673058dc0e1 100644 (file)
--- a/test/maxset.expect
+++ b/test/maxset.expect
@@ -2,11 +2,14 @@
 Finished LCLint checking --- no code errors found
 
 maxsetnoannotations.c: (in function noancopy)
-maxsetnoannotations.c:4:1: Unresolved constraint:
-    Lclint is unable to resolve Requires: : MAXSET ((a @ maxsetnoannotations.c:4
-    :9 ) )  >=  MAXREAD ((b @ maxsetnoannotations.c:4:11 ) ) needed to satisfy
-    Requires: : MAXSET ((a @ maxsetnoannotations.c:4:9 ) )  >=  MAXREAD ((b @
-    maxsetnoannotations.c:4:11 ) ) derived from strcpy precondition: Requires:
-    : MAXSET ((<parameter 1> ) )  >=  MAXREAD ((<parameter 2> ) )
+maxsetnoannotations.c:4:1: Possible out-of-bounds store.  Unable to resolve
+    constraint:
+    requires: : maxSet ((a @ maxsetnoannotations.c:4:9 ) )  >=  maxRead ((b @
+    maxsetnoannotations.c:4:11 ) )
+     needed to satisfy precondition:
+    requires: : maxSet ((a @ maxsetnoannotations.c:4:9 ) )  >=  maxRead ((b @
+    maxsetnoannotations.c:4:11 ) )
+     derived from strcpy precondition: requires: :
+    maxSet ((<parameter 1> ) )  >=  maxRead ((<parameter 2> ) )
 
 Finished LCLint checking --- 1 code error found

diff --git a/test/maxset/.lclintrc b/test/maxset/.lclintrc
index 7512d0fca237c0107405e1c7f325d5d9b805f6b7..3733a1e3e040474a8d4457dc5118280a6d8e89e0 100644 (file)
--- a/test/maxset/.lclintrc
+++ b/test/maxset/.lclintrc
@@ -1,2 +1,2 @@
 -no-lib
-+fcnconstraint
++arrayBounds

diff --git a/test/modtest.lcs b/test/modtest.lcs
index aaa0bcbb7ba1b83a1db9709db174c2bc8ec15d56..441a325a123b52f7147ac65abc42ca74e703f43d 100644 (file)
--- a/test/modtest.lcs
+++ b/test/modtest.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/moreBufferTests.expect b/test/moreBufferTests.expect
index faf52ba171ba7cc356dcecf9bc18e5e1affedd27..23697c16a60a93dd0492a9a4b3869ac91d7bb2ec 100644 (file)
--- a/test/moreBufferTests.expect
+++ b/test/moreBufferTests.expect
@@ -3,32 +3,40 @@ unrecogCall.c: (in function foo)
 unrecogCall.c:8:3: Unrecognized identifier: bar
 initialization.c: (in function initialization)
 initialization.c:5:10: Variable g declared but not used
-initialization.c:8:3: Unresolved constraint:
-    Lclint is unable to resolve Requires: : MAXSET ((d @ initialization.c:3:14
-    ) )  >=  ( 2 )  needed to satisfy Requires: :
-    MAXSET ((f @ initialization.c:8:3 ) )  >=  ( 2 ) 
-initialization.c:5:14: Unresolved constraint:
-    Lclint is unable to resolve Requires: : MAXREAD ((d @ initialization.c:3:14
-    ) )  >=  ( 22 )  needed to satisfy Requires: :
-    MAXREAD ((e @ initialization.c:5:14 ) )  >=  ( 22 ) 
+initialization.c:8:3: Possible out-of-bounds store.  Unable to resolve
+    constraint:
+    requires: : maxSet ((d @ initialization.c:3:14 ) )  >=  ( 2 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((f @ initialization.c:8:3 ) )  >=  ( 2 ) 
+initialization.c:5:14: Possible out-of-bounds read.  Unable to resolve
+    constraint:
+    requires: : maxRead ((d @ initialization.c:3:14 ) )  >=  ( 22 ) 
+     needed to satisfy precondition:
+    requires: : maxRead ((e @ initialization.c:5:14 ) )  >=  ( 22 ) 
 simplifyTest.c: (in function fooSub)
-simplifyTest.c:3:3: Unresolved constraint:
-    Lclint is unable to resolve Requires: : MAXSET ((s @ simplifyTest.c:3:3 ) )
-     >=  (i @ simplifyTest.c:3:5 )  needed to satisfy Requires: :
-    MAXSET ((s @ simplifyTest.c:3:3 ) )  >=  (i @ simplifyTest.c:3:5 ) 
+simplifyTest.c:3:3: Possible out-of-bounds store.  Unable to resolve
+    constraint:
+    requires: : maxSet ((s @ simplifyTest.c:3:3 ) )  >=  (i @
+    simplifyTest.c:3:5 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((s @ simplifyTest.c:3:3 ) )  >=  (i @
+    simplifyTest.c:3:5 ) 
 simplifyTest.c: (in function fooAdd)
-simplifyTest.c:10:3: Unresolved constraint:
-    Lclint is unable to resolve Requires: : MAXSET ((s @ simplifyTest.c:10:3 )
-    )  >=  ((i @ simplifyTest.c:10:5 ) ) + (( 2 ) ) needed to satisfy Requires:
-    : MAXSET ((s @ simplifyTest.c:10:3 ) )  >=  ((i @ simplifyTest.c:10:5 ) ) +
-    (( 2 ) )
+simplifyTest.c:10:3: Possible out-of-bounds store.  Unable to resolve
+    constraint:
+    requires: : maxSet ((s @ simplifyTest.c:10:3 ) )  >=  ((i @
+    simplifyTest.c:10:5 ) ) + (( 2 ) )
+     needed to satisfy precondition:
+    requires: : maxSet ((s @ simplifyTest.c:10:3 ) )  >=  ((i @
+    simplifyTest.c:10:5 ) ) + (( 2 ) )
 strncatNotReallyGood.c: (in function NotGoodfunc)
 strncatNotReallyGood.c:4:29: Passed storage buffer not completely defined
                                 (*buffer is undefined): strncat (buffer, ...)
-strncatNotReallyGood.c:4:21: Unresolved constraint:
-    Lclint is unable to resolve Requires: :
-    MAXREAD ((buffer @ strncatNotReallyGood.c:4:29 ) )  <=  ( 0 )  needed to
-    satisfy Requires: : MAXSET ((buffer @ strncatNotReallyGood.c:4:29 ) )  >= 
-    (MAXREAD ((buffer @ strncatNotReallyGood.c:4:29 ) )) + (( 255 ) )
+strncatNotReallyGood.c:4:21: Possible out-of-bounds store.  Unable to resolve
+    constraint:
+    requires: : maxRead ((buffer @ strncatNotReallyGood.c:4:29 ) )  <=  ( 0 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((buffer @ strncatNotReallyGood.c:4:29 ) )  >=  (maxRead
+    ((buffer @ strncatNotReallyGood.c:4:29 ) )) + (( 255 ) )
 
 Finished LCLint checking --- 8 code errors found

diff --git a/test/mut.lcs b/test/mut.lcs
index 8420ed1987812ca84fbcb35d01256b40f2473c56..7b5577934584dd33609464f1c23f8dd5ce936ffd 100644 (file)
--- a/test/mut.lcs
+++ b/test/mut.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/mut.lh b/test/mut.lh
index 3616b5de240f90d2078edb94e2d072214ade3593..1815e5ceb151c00e0af4c4aebf85325d25dded95 100644 (file)
--- a/test/mut.lh
+++ b/test/mut.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 # include "bool.h"
 
 

diff --git a/test/null6.lcd b/test/null6.lcd
index 532d27e44ae275ff708cc6b8bf4b56c22acb2145..479cbb8489fd450ba8f61ddb655c8a38fd5cb9cd 100644 (file)
--- a/test/null6.lcd
+++ b/test/null6.lcd
@@ -1,5 +1,5 @@
 ;;LCLint Dump: null6.lcd
-;;LCLint 3.0.0.8 --- 19 July 2001
+;;LCLint 3.0.0.9 --- 23 July 2001
 ;;lib:168
 ;;ctTable
 0 u-2 19 38

diff --git a/test/null6.lcs b/test/null6.lcs
index ae317b18db7dc6594d74c7f65689989e8ff06308..90c0a3a8347bc86e22658e07c34576909dd6261b 100644 (file)
--- a/test/null6.lcs
+++ b/test/null6.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/observer.lcs b/test/observer.lcs
index 08f4c798b9896963bc23e833bfe370e09e75f736..84c37f50dc91524d8300fa1b8f00ec2f9afc7106 100644 (file)
--- a/test/observer.lcs
+++ b/test/observer.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/oldstyle.lcs b/test/oldstyle.lcs
index 1a03b0acb0a05a686729c695552f1dca0b212ccb..a0e95bf3014471f888a3de26696286c24370a650 100644 (file)
--- a/test/oldstyle.lcs
+++ b/test/oldstyle.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/outglob.lcs b/test/outglob.lcs
index 1cc122cd573817b7e51537a9355c29b219821935..b3f0f0ca54b3b1e4f67d20fe5b37be4f84e721ad 100644 (file)
--- a/test/outglob.lcs
+++ b/test/outglob.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/outparam.lcs b/test/outparam.lcs
index bcf37b39121098169e8a571d59e32e4c7bf80a6e..e520adce2b97b483d5245208487d4b4af5100bb9 100644 (file)
--- a/test/outparam.lcs
+++ b/test/outparam.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/repexpose.lcs b/test/repexpose.lcs
index aadd27f105742b981b349610c241ca3f32b645fb..be48846943511fb32f44d6c0a1f3fa2b6cead349 100644 (file)
--- a/test/repexpose.lcs
+++ b/test/repexpose.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/repexpose.lh b/test/repexpose.lh
index 6b4a0e79356d98e2be6cebd09614640675cc1336..ed3b21619945e734da0b2b66d07be5b0895057df 100644 (file)
--- a/test/repexpose.lh
+++ b/test/repexpose.lh
@@ -1,4 +1,4 @@
-/* Output from LCLint 3.0.0.8 */
+/* Output from LCLint 3.0.0.9 */
 # include "bool.h"
 
 

diff --git a/test/simplebufferConstraintTests.expect b/test/simplebufferConstraintTests.expect
index 6272fb833941180c947929345443785c8254c32d..6220f7c61053261b7171e64693084b782f97361a 100644 (file)
--- a/test/simplebufferConstraintTests.expect
+++ b/test/simplebufferConstraintTests.expect
@@ -3,25 +3,27 @@ m.c: (in function t)
 m.c:9:1: Index of possibly null pointer f: f
    m.c:8:5: Storage f may become null
 sizeof.c: (in function f)
-sizeof.c:17:1: Unresolved constraint:
-    Lclint is unable to resolve Requires: :
-    ( 2 )   >=  ( 3 )  needed to satisfy Requires: : MAXSET ((x @ sizeof.c:17:1
-    ) )  >=  ( 3 ) 
+sizeof.c:17:1: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : ( 2 )   >=  ( 3 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((x @ sizeof.c:17:1 ) )  >=  ( 3 ) 
 test3.c:2:6: Function t defined more than once
    m.c:11:1: Previous definition of t
 test3.c: (in function t)
-test3.c:9:3: Unresolved constraint:
-    Lclint is unable to resolve Requires: :
-    ( 99 )   >=  ( 101 )  needed to satisfy Requires: : MAXSET ((g @
-    test3.c:9:3 ) )  >=  ( 101 ) 
+test3.c:9:3: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : ( 99 )   >=  ( 101 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((g @ test3.c:9:3 ) )  >=  ( 101 ) 
 test7.c:2:6: Function t defined more than once
    m.c:11:1: Previous definition of t
 test7.c: (in function t)
-test7.c:8:3: Unresolved constraint:
-    Lclint is unable to resolve Requires: : MAXSET ((j @ test7.c:8:3 ) )  >=  (
-    0 )  needed to satisfy Requires: : MAXSET ((j @ test7.c:8:3 ) )  >=  ( 0 ) 
-test7.c:6:3: Unresolved constraint:
-    Lclint is unable to resolve Requires: : MAXSET ((g @ test7.c:4:3 ) )  >=  (
-    4 )  needed to satisfy Requires: : MAXSET ((g @ test7.c:6:3 ) )  >=  ( 2 ) 
+test7.c:8:3: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : maxSet ((j @ test7.c:8:3 ) )  >=  ( 0 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((j @ test7.c:8:3 ) )  >=  ( 0 ) 
+test7.c:6:3: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : maxSet ((g @ test7.c:4:3 ) )  >=  ( 4 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((g @ test7.c:6:3 ) )  >=  ( 2 ) 
 
 Finished LCLint checking --- 7 code errors found

diff --git a/test/sizeoftest.expect b/test/sizeoftest.expect
index e9969c8389beef2984179cc98914961c39c7250a..223775ed85ce5974bb4029224cb2bc2a56e817ba 100644 (file)
--- a/test/sizeoftest.expect
+++ b/test/sizeoftest.expect
@@ -1,8 +1,8 @@
 
 sizeof.c: (in function main)
-sizeof.c:6:2: Unresolved constraint:
-    Lclint is unable to resolve Requires: :
-    ( 2 )   >=  ( 3 )  needed to satisfy Requires: : MAXSET ((x @ sizeof.c:6:2
-    ) )  >=  ( 3 ) 
+sizeof.c:6:2: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : ( 2 )   >=  ( 3 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((x @ sizeof.c:6:2 ) )  >=  ( 3 ) 
 
 Finished LCLint checking --- 1 code error found

diff --git a/test/sizeoftest.out b/test/sizeoftest.out
index e9969c8389beef2984179cc98914961c39c7250a..223775ed85ce5974bb4029224cb2bc2a56e817ba 100644 (file)
--- a/test/sizeoftest.out
+++ b/test/sizeoftest.out
@@ -1,8 +1,8 @@
 
 sizeof.c: (in function main)
-sizeof.c:6:2: Unresolved constraint:
-    Lclint is unable to resolve Requires: :
-    ( 2 )   >=  ( 3 )  needed to satisfy Requires: : MAXSET ((x @ sizeof.c:6:2
-    ) )  >=  ( 3 ) 
+sizeof.c:6:2: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : ( 2 )   >=  ( 3 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((x @ sizeof.c:6:2 ) )  >=  ( 3 ) 
 
 Finished LCLint checking --- 1 code error found

diff --git a/test/special.lcs b/test/special.lcs
index 8d4ebb4d663a3fbef9a3245e91c9f3fe5732f040..8b84f107065710ffb3e8821b1eec93b75adde1c6 100644 (file)
--- a/test/special.lcs
+++ b/test/special.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/strchr/strchr.c b/test/strchr/strchr.c
index 0f6f0e24fd40c2b61a9a147e384fa51d82713b4b..4c873d2dd84c8617e16603c25e726902cad6e552 100644 (file)
--- a/test/strchr/strchr.c
+++ b/test/strchr/strchr.c
@@ -1,4 +1,4 @@
-#include "../../lib/ansi.h"
+
 
 void func () {
   char *c;

diff --git a/test/tests2.2/bool.lcs b/test/tests2.2/bool.lcs
index 06fe0766859c8736ac2a0da1189e7fdbb4632c92..d5907186cf632db8b316e1d059e7c58c4cdb00a9 100644 (file)
--- a/test/tests2.2/bool.lcs
+++ b/test/tests2.2/bool.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/tests2.4/subdir/main.lcs b/test/tests2.4/subdir/main.lcs
index 3e35e0d896a9bffb7de57feb876ce12dd32f0a63..839abfd701da205fb3a64800f77cc9d48e1bd753 100644 (file)
--- a/test/tests2.4/subdir/main.lcs
+++ b/test/tests2.4/subdir/main.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/tests2.5/newlint.lcd b/test/tests2.5/newlint.lcd
index c94f7b52e6e94da4713b79d81abc0c2ebe7e84a1..022460ce0ec83b2a2efa553cb7214a0136b621c4 100644 (file)
--- a/test/tests2.5/newlint.lcd
+++ b/test/tests2.5/newlint.lcd
@@ -1,5 +1,5 @@
 ;;LCLint Dump: newlint.lcd
-;;LCLint 3.0.0.8 --- 19 July 2001
+;;LCLint 3.0.0.9 --- 23 July 2001
 ;;lib:168
 ;;ctTable
 0 u-2 19 38

diff --git a/test/tq.lcs b/test/tq.lcs
index 5b180fa51f97835646121d7678d9c712937d957d..a355c9b946352c41d9523833b5e168446df1593b 100644 (file)
--- a/test/tq.lcs
+++ b/test/tq.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil

diff --git a/test/ud2.lcs b/test/ud2.lcs
index 0b3efd8d67c6313200b0b87aef7f682f1263bc96..7df07676812846a0e301313f5932111cc09e33e5 100644 (file)
--- a/test/ud2.lcs
+++ b/test/ud2.lcs
@@ -1,4 +1,4 @@
-%PASSED Output from LCLint 3.0.0.8
+%PASSED Output from LCLint 3.0.0.9
 %LCLimports 
 %LCLSortTable
 %LCLsort bool immutable nil nil