*** empty log message ***

[splint.git] / src / constraint.c

diff --git a/src/constraint.c b/src/constraint.c
index aaaa9e68997cd12c836cdf2e92d5a7b4e80ffd21..fc6e7be5122c8e505c55ba1a1264ef9243624ce5 100644 (file)
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -21,8 +21,9 @@
 static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
 
 
-static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
-     /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
+static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
+     /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/
+     /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
      
 /*  constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant) */
      
@@ -74,7 +75,7 @@ static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode
   char *t;
   int c;
   constraint ret;
-  ret = constraint_makeNew();
+  ret = constraint_makeNew ();
   llassert (constraintExpr_isDefined(l) );
       
   ret->lexpr = constraintExpr_copy (l);
@@ -225,7 +226,8 @@ void constraint_overWrite (constraint c1, constraint c2)
 
 
 static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
-     /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
+     /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/ 
+     /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
 {
   constraint ret;
   ret = dmalloc(sizeof (*ret) );
@@ -240,7 +242,7 @@ static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
   return ret;
 }
 
-constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
+constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
 {
     
   if (c->generatingExpr == NULL)
@@ -307,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)
@@ -723,37 +728,34 @@ void constraint_printError (constraint c, fileloc loc)
 
   errorLoc = loc;
 
-  loc = NULL;
-
   temp = constraint_getFileloc(c);
 
   if (fileloc_isDefined(temp) )
     {
       errorLoc = temp;
-      
-      if (c->post)
-       {
-         voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
-       }
-      else
-       {
-         voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
-       }
+    }
+  else
+    {
+      llassert(FALSE);
+      DPRINTF(( message("constraint %s had undefined fileloc %s", constraint_print(c), fileloc_unparse(temp) ) ));
       fileloc_free(temp);
-      errorLoc = NULL;
+      errorLoc = fileloc_copy(errorLoc);
+    }
+      
+  if (c->post)
+    {
+      voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
     }
   else
     {
-      if (c->post)
-       {
-         voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
-       }
+      if (constraint_hasMaxSet (c) )
+       voptgenerror (FLG_ARRAYBOUNDS, string, errorLoc);
       else
-       {
-         voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
-       }
-      errorLoc = NULL;
+       voptgenerror (FLG_ARRAYBOUNDSREAD, string, errorLoc);
     }
+
+  fileloc_free(errorLoc);
+
 }
 
 
@@ -767,6 +769,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)
        {
@@ -774,7 +777,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) )
                                        ) );
          
@@ -821,32 +824,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;
 }
@@ -858,11 +867,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,
@@ -1058,6 +1067,7 @@ constraint constraint_undump (FILE *f)
   c->expr =  expr;
 
   free(os);
+  c = constraint_preserveOrig(c);
   return c;
 }
 
@@ -1086,3 +1096,46 @@ void constraint_dump (/*@observer@*/ constraint c,  FILE *f)
 }
 
 
+int constraint_compare (/*@observer@*/ /*@temp@*/ constraint * c1, /*@observer@*/ /*@temp@*/ constraint * c2) /*@*/
+{
+  fileloc loc1, loc2;
+
+  int ret;
+  
+  llassert(constraint_isDefined(*c1) );
+  llassert(constraint_isDefined(*c2) );
+
+  if (constraint_isUndefined(*c1) )
+    {
+        if (constraint_isUndefined(*c2) )
+         return 0;
+       else
+         return 1;
+    }
+
+  if (constraint_isUndefined(*c2) )
+    {
+      return -1;
+    }
+    
+  loc1 = constraint_getFileloc(*c1);
+  loc2 = constraint_getFileloc(*c2);
+
+  ret = fileloc_compare(loc1, loc2);
+
+  fileloc_free(loc1);
+  fileloc_free(loc2);
+    
+  return ret;
+}
+
+
+bool constraint_isPost  (/*@observer@*/ /*@temp@*/ constraint c)
+{
+  llassert(constraint_isDefined(c) );
+
+  if (constraint_isUndefined(c) )
+    return FALSE;
+  
+  return (c->post);
+}