]> andersk Git - splint.git/blobdiff - src/constraint.c
Added check of user specified post conditions.
[splint.git] / src / constraint.c
index ec5eb02d513dba3fd74a7fa7a2fa02060bc6b261..a39808fa8b7c152d04cd54a7e94a2a966d2c6097 100644 (file)
@@ -1,5 +1,5 @@
 /*
-** constraintList.c
+** constraint.c
 */
 
 //#define DEBUGPRINT 1
 /*@-fcnuse*/
 /*@-assignexpose*/
 
-constraint constraint_makeNew (void);
+/*@access exprNode @*/
 
 
-constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant)
+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 @*/;
      
-{
-  char *t;
-  int c;
-  constraint ret;
-  ret = constraint_makeNew();
-  llassert (sRef_isValid(x) );
-  if (!sRef_isValid(x))
-    return ret;
+/*  constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant) */
+     
+/*  { */
+/*    char *t; */
+/*    int c; */
+/*    constraint ret; */
+/*    ret = constraint_makeNew(); */
+/*    llassert (sRef_isValid(x) ); */
+/*    if (!sRef_isValid(x)) */
+/*      return ret; */
  
     
-  ret->lexpr = constraintExpr_makeTermsRef (x);
-  #warning fix abstraction
+/*    ret->lexpr = constraintExpr_makeTermsRef (x); */
+/*    #warning fix abstraction */
 
-  if (relOp.tok == GE_OP)
-      ret->ar = GTE;
-  else if (relOp.tok == LE_OP)
-    ret->ar = LTE;
-  else if (relOp.tok == EQ_OP)
-    ret->ar = EQ;
-  else
-  llfatalbug("Unsupported relational operator");
+/*    if (relOp.tok == GE_OP) */
+/*        ret->ar = GTE; */
+/*    else if (relOp.tok == LE_OP) */
+/*      ret->ar = LTE; */
+/*    else if (relOp.tok == EQ_OP) */
+/*      ret->ar = EQ; */
+/*    else */
+/*      llfatalbug(message ("Unsupported relational operator") ); */
 
 
-  t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
-  c = atoi( t );
-  ret->expr = constraintExpr_makeIntLiteral (c);
+/*    t =  cstring_toCharsSafe (exprNode_unparse(cconstant)); */
+/*    c = atoi( t ); */
+/*    ret->expr = constraintExpr_makeIntLiteral (c); */
 
-  ret->post = TRUE;
-  //  ret->orig = ret;
-  DPRINTF(("GENERATED CONSTRAINT:"));
-  DPRINTF( (message ("%s", constraint_print(ret) ) ) );
-  return ret;
-}
+/*    ret->post = TRUE; */
+/*    //  ret->orig = ret; */
+/*    DPRINTF(("GENERATED CONSTRAINT:")); */
+/*    DPRINTF( (message ("%s", constraint_print(ret) ) ) ); */
+/*    return ret; */
+/*  } */
 
-constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
-     
+constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)    
 {
   char *t;
   int c;
   constraint ret;
   ret = constraint_makeNew();
-  llassert (l);
-  if (!l)
-    return ret;
-    
+  llassert (l!=NULL);
+      
   ret->lexpr = constraintExpr_copy (l);
   #warning fix abstraction
 
@@ -80,7 +79,7 @@ constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconsta
   else if (relOp.tok == EQ_OP)
     ret->ar = EQ;
   else
-  llfatalbug("Unsupported relational operator");
+  llfatalbug(message("Unsupported relational operator") );
 
 
   t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
@@ -94,15 +93,26 @@ constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconsta
   return ret;
 }
 
+bool constraint_same (constraint c1, constraint c2)
+{
+  
+  if (c1->ar != c2->ar)
+    return FALSE;
+
+  if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
+    return FALSE;
+
+  if (!constraintExpr_similar (c1->expr, c2->expr) )
+    return FALSE;
+
+  return TRUE;
+}
 
 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)     
 {
   constraint ret;
   ret = constraint_makeNew();
-  llassert (l);
-  if (!l)
-    return ret;
+  llassert (l !=NULL);
     
   ret->lexpr = constraintExpr_copy (l);
   #warning fix abstraction
@@ -114,11 +124,16 @@ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r
   else if (relOp.tok == EQ_OP)
     ret->ar = EQ;
   else
-  llfatalbug("Unsupported relational operator");
+  llfatalbug( message("Unsupported relational operator") );
 
   ret->expr = constraintExpr_copy (r);
 
   ret->post = TRUE;
+
+  ret->orig = constraint_copy(ret);
+
+  ret = constraint_simplify (ret);
+  
   //  ret->orig = ret;
   DPRINTF(("GENERATED CONSTRAINT:"));
   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
@@ -128,43 +143,78 @@ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r
 constraint constraint_copy (constraint c)
 {
   constraint ret;
+
+  llassert (constraint_isDefined(c) );
+  // TPRINTF((message("Copying constraint %q", constraint_print) ));
+  
   ret = constraint_makeNew();
   ret->lexpr = constraintExpr_copy (c->lexpr);
   ret->ar = c->ar;
   ret->expr =  constraintExpr_copy (c->expr);
   ret->post = c->post;
+  ret->generatingExpr = exprNode_fakeCopy(c->generatingExpr);
+  
   /*@i33 fix this*/
   if (c->orig != NULL)
     ret->orig = constraint_copy (c->orig);
   else
     ret->orig = NULL;
+
+  if (c->or != NULL)
+    ret->or = constraint_copy (c->or);
+  else
+    ret->or = NULL;
+
+  ret->fcnPre = c->fcnPre;
+  
   return ret;
 }
 
 /*like copy expect it doesn't allocate memory for the constraint*/
 
-void constraint_overWrite (constraint c1, constraint c2)
+void constraint_overWrite (constraint c1, constraint c2) 
 {
+  llassert (constraint_isDefined(c1) );
+
+  llassert (c1 != c2);
+
+  DPRINTF((message("OverWriteing constraint %q with %q", constraint_print(c1),
+                  constraint_print(c2) ) ));
+  
+  constraintExpr_free(c1->lexpr);
+  constraintExpr_free(c1->expr);
+  
   c1->lexpr = constraintExpr_copy (c2->lexpr);
   c1->ar = c2->ar;
   c1->expr =  constraintExpr_copy (c2->expr);
   c1->post = c2->post;
-  /*@i33 fix this*/
+
+  if (c1->orig != NULL)
+    constraint_free (c1->orig);
+
   if (c2->orig != NULL)
     c1->orig = constraint_copy (c2->orig);
   else
     c1->orig = NULL;
 
-}
+  /*@i33 make sure that the or is freed correctly*/
+  if (c1->or != NULL)
+    constraint_free (c1->or);
 
-bool constraint_resolve (/*@unused@*/ constraint c)
-{
-  return FALSE;
+  if (c2->or != NULL)
+    c1->or = constraint_copy (c2->or);
+  else
+    c1->or = NULL;
+
+  c1->fcnPre = c2->fcnPre;
+  
+  c1->generatingExpr = c2->generatingExpr;
 }
 
 
 
-constraint constraint_makeNew (void)
+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 ret;
   ret = dmalloc(sizeof (*ret) );
@@ -173,16 +223,90 @@ constraint constraint_makeNew (void)
   ret->ar = LT;
   ret->post = FALSE;
   ret->orig = NULL;
-  /*@i23*/return ret;
+  ret->or = NULL;
+  ret->generatingExpr = NULL;
+  ret->fcnPre = NULL;
+  return ret;
+}
+
+constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
+{
+    
+  if (c->generatingExpr == NULL)
+    {
+      c->generatingExpr = exprNode_fakeCopy(e);
+      DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
+    }
+  else
+    {
+      DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
+    }
+  return c;
+}
+
+constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
+{
+
+  if (c->orig != constraint_undefined)
+    {
+      c->orig = constraint_addGeneratingExpr(c->orig, e);
+    }
+  else
+    {
+      DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
+    }
+  return c;
 }
 
+
+
+constraint constraint_setFcnPre (/*@returned@*/ constraint c )
+{
+
+  if (c->orig != constraint_undefined)
+    {
+      c->orig->fcnPre = TRUE;
+    }
+  else
+    {
+      c->fcnPre = TRUE;
+      TPRINTF(( message("Warning Setting fcnPre directly") ));
+    }
+  return c;
+}
+
+
+
+
 fileloc constraint_getFileloc (constraint c)
 {
+  if (exprNode_isDefined(c->generatingExpr) )
+    return (fileloc_copy (exprNode_getfileloc (c->generatingExpr) ) );
+           
   return (constraintExpr_getFileloc (c->lexpr) );
 
 
 }
 
+static bool checkForMaxSet (constraint c)
+{
+  if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
+    return TRUE;
+
+  return FALSE;
+}
+
+bool constraint_hasMaxSet(constraint c)
+{
+  if (c->orig != NULL)
+    {
+      if (checkForMaxSet(c->orig) )
+       return TRUE;
+    }
+
+  return (checkForMaxSet(c) );
+}
+
 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
 {
   constraint ret = constraint_makeNew();
@@ -192,6 +316,7 @@ constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
   ret->ar    = GTE;
   ret->expr  = constraintExpr_makeValueExpr (ind);
+  ret->post = FALSE;
   return ret;
 }
 
@@ -202,16 +327,16 @@ constraint constraint_makeWriteSafeInt (exprNode po, int ind)
  
   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
   ret->ar = GTE;
-  ret->expr =  constraintExpr_makeValueInt (ind);
+  ret->expr =  constraintExpr_makeIntLiteral (ind);
   /*@i1*/return ret;
 }
 
-constraint constraint_makeSRefSetBufferSize (sRef s, int size)
+constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
 {
  constraint ret = constraint_makeNew();
  ret->lexpr = constraintExpr_makeSRefMaxset (s);
  ret->ar = EQ;
- ret->expr =  constraintExpr_makeValueInt (size);
+ ret->expr =  constraintExpr_makeIntLiteral ((int)size);
  ret->post = TRUE;
  /*@i1*/return ret;
 }
@@ -221,9 +346,9 @@ constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
   constraint ret = constraint_makeNew();
 
  
-  ret->lexpr = constraintExpr_makeSRefMaxset (s);
+  ret->lexpr = constraintExpr_makeSRefMaxset ( s );
   ret->ar = GTE;
-  ret->expr =  constraintExpr_makeValueInt (ind);
+  ret->expr =  constraintExpr_makeIntLiteral (ind);
   ret->post = TRUE;
   /*@i1*/return ret;
 }
@@ -263,14 +388,26 @@ constraint constraint_makeReadSafeInt ( exprNode po, int ind)
   
   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
   ret->ar    = GTE;
-  ret->expr  = constraintExpr_makeValueInt (ind);
+  ret->expr  = constraintExpr_makeIntLiteral (ind);
+  ret->post = FALSE;
   return ret;
 }
 
-constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
+constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
 {
   constraint ret = constraint_makeNew();
 
+  ret->lexpr = constraintExpr_makeSRefMaxRead (s );
+  ret->ar = GTE;
+  ret->expr =  constraintExpr_makeIntLiteral (ind);
+  ret->post = TRUE;
+  /*@i1*/return ret;
+}
+
+constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
+{
+  constraint ret;
 
   e1 = exprNode_fakeCopy (e1);
   t2 = exprNode_fakeCopy (t2);
@@ -285,27 +422,47 @@ constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, filelo
   return ret;
 }
 
+static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint,  arithType  ar)
+{
+
+  constraint ret;
+  
+  llassert(c1 && c2);
+  //  llassert(sequencePoint);
+
+  ret = constraint_makeNew();
+  
+  ret->lexpr = c1;
+  ret->ar = ar;
+  ret->post = TRUE;
+  ret->expr =  c2;
+  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+  return ret;
+}
 
 static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint,  arithType  ar)
 {
-  constraint ret = constraint_makeNew();
+  constraintExpr c1, c2;
+  constraint ret;
   exprNode e;
-  
-  e = exprNode_fakeCopy(e1);
+
   if (! (e1 && e2) )
     {
       llcontbug((message("null exprNode, Exprnodes are %s and %s",
                       exprNode_unparse(e1), exprNode_unparse(e2) )
               ));
     }
-                      
-  ret->lexpr = constraintExpr_makeValueExpr (e);
-  ret->ar = ar;
-  ret->post = TRUE;
-  e = exprNode_fakeCopy(e2);
-  ret->expr =  constraintExpr_makeValueExpr (e);
+
+  //  llassert (sequencePoint);
+  
+  e  =  exprNode_fakeCopy(e1);
+  c1 =  constraintExpr_makeValueExpr (e);
+  
+  e  =  exprNode_fakeCopy(e2);
+  c2 =  constraintExpr_makeValueExpr (e);
+
+  ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
   
-  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
   return ret;
 }
 
@@ -320,7 +477,16 @@ constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequenc
 /*make constraint ensures e1 < e2 */
 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 {
- return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) );
+  constraintExpr t1, t2;
+
+  t1 = constraintExpr_makeValueExpr (e1);
+  t2 = constraintExpr_makeValueExpr (e2);
+
+  /*change this to e1 <= (e2 -1) */
+
+  t2 = constraintExpr_makeDecConstraintExpr (t2);
+  
+ return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
 }
 
 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
@@ -330,7 +496,17 @@ constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc
 
 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 {
- return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) );
+  constraintExpr t1, t2;
+
+  t1 = constraintExpr_makeValueExpr (e1);
+  t2 = constraintExpr_makeValueExpr (e2);
+
+
+  /* change this to e1 >= (e2 + 1) */
+  t2 = constraintExpr_makeIncConstraintExpr (t2);
+  
+  
+ return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
 }
 
 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
@@ -341,6 +517,11 @@ constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, file
 
 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
 {
+  constraintList_free(dst->ensuresConstraints);
+  constraintList_free(dst->requiresConstraints);
+  constraintList_free(dst->trueEnsuresConstraints);
+  constraintList_free(dst->falseEnsuresConstraints);
+  
   dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
   dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
   dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
@@ -384,6 +565,29 @@ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc seq
 }
 
 
+void constraint_free (/*@only@*/ /*@notnull@*/ constraint c)
+{
+  llassert(constraint_isDefined (c) );
+
+
+  if (constraint_isDefined(c->orig) )
+    constraint_free (c->orig);
+  if ( constraint_isDefined(c->or) )
+    constraint_free (c->or);
+
+  
+  constraintExpr_free(c->lexpr);
+  constraintExpr_free(c->expr);
+
+  c->orig = NULL;
+  c->or = NULL;
+  c->lexpr = NULL;
+  c->expr  = NULL;
+
+  free (c);
+  
+}
+
 
 // constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 // {
@@ -400,7 +604,7 @@ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc seq
 // }
 
 
-cstring arithType_print (arithType ar)
+cstring arithType_print (arithType ar) /*@*/
 {
   cstring st = cstring_undefined;
   switch (ar)
@@ -433,51 +637,165 @@ cstring arithType_print (arithType ar)
   return st;
 }
 
-void constraint_printError (constraint c, fileloc loc)
+
+void constraint_printErrorPostCondition (constraint c, fileloc loc)
 {
   cstring string;
-
-  string = constraint_printDetailed (c);
+  fileloc errorLoc, temp;
   
-  if (c->post)
+  string = constraint_printDetailedPostCondition (c);
+
+  errorLoc = loc;
+
+  loc = NULL;
+
+  temp = constraint_getFileloc(c);
+
+  if (fileloc_isDefined(temp) )
     {
-       voptgenerror (FLG_FUNCTIONPOST, string, loc);
+      errorLoc = temp;
+      voptgenerror (  FLG_CHECKPOST, string, errorLoc);
+      fileloc_free(temp);
     }
   else
     {
-      voptgenerror (FLG_FUNCTIONCONSTRAINT, string, loc);
+      voptgenerror (  FLG_CHECKPOST, string, errorLoc);
     }
+}
+
+
+
+
+void constraint_printError (constraint c, fileloc loc)
+{
+  cstring string;
+  fileloc errorLoc, temp;
+  
+  string = constraint_printDetailed (c);
+
+  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);
+       }
+      fileloc_free(temp);
+    }
+  else
+    {
+      if (c->post)
+       {
+         voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
+       }
+      else
+       {
+         voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
+       }
+    }
 }
 
-cstring  constraint_printDetailed (constraint c)
+
+cstring constraint_printDeep (constraint c)
 {
   cstring st = cstring_undefined;
 
+  st = constraint_print(c);
+
+  if (c->orig != constraint_undefined)
+    {
+      if (!c->post)
+       {
+         if (c->orig->fcnPre)
+           st = cstring_concatFree(st, (message(" derived from %s precondition: %q", exprNode_unparse(c->orig->generatingExpr), constraint_printDeep(c->orig) )
+                                        ) );
+         else
+           st = cstring_concatFree(st,(message(" needed to satisfy %q",
+                                               constraint_printDeep(c->orig) )
+                                       ) );
+         
+       }
+      else
+       {
+         st = cstring_concatFree(st,(message("derived from: %q",
+                                             constraint_printDeep(c->orig) )
+                                     ) );
+       }
+    }
+
+  return st;  
+
+}
+
+cstring  constraint_printDetailedPostCondition (constraint c)
+{
+  cstring st = cstring_undefined;
+
+  st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) );
+  if (context_getFlag (FLG_CONSTRAINTLOCATION) )
+    {
+      cstring temp;
+      // llassert (c->generatingExpr);
+      temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
+                     exprNode_unparse(c->generatingExpr) );
+      st = cstring_concatFree (st, temp);
+
+      if (constraint_hasMaxSet(c) )
+       {
+         temp = message ("Has MaxSet\n");
+         st = cstring_concatFree (st, temp);
+       }
+    }
+  return st;
+}
+
+cstring  constraint_printDetailed (constraint c)
+{
+  cstring st = cstring_undefined;
 
   if (!c->post)
     {
-    if (c->orig)  
-      st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisfy %s", constraint_print (c), constraint_print(c->orig) );
-    else
-      st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
-      
+      st = message ("Unresolved constraint:\nLclint is unable to resolve %q", constraint_printDeep (c) );
     }
   else
     {
-      if (c->orig)
-       st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
-      else
-       st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));    
+      st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
+    }
+
+  if (context_getFlag (FLG_CONSTRAINTLOCATION) )
+    {
+      cstring temp;
+      // llassert (c->generatingExpr);
+      temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
+                     exprNode_unparse(c->generatingExpr) );
+      st = cstring_concatFree (st, temp);
+
+      if (constraint_hasMaxSet(c) )
+       {
+         temp = message ("Has MaxSet\n");
+         st = cstring_concatFree (st, temp);
+       }
     }
   return st;
 }
 
-cstring  constraint_print (constraint c) /*@*/
+/*@only@*/ cstring  constraint_print (constraint c) /*@*/
 {
   cstring st = cstring_undefined;
   cstring type = cstring_undefined;
-  llassert (c);
+  llassert (c !=NULL);
   if (c->post)
     {
       type = cstring_makeLiteral ("Ensures: ");
@@ -486,7 +804,7 @@ cstring  constraint_print (constraint c) /*@*/
     {
       type = cstring_makeLiteral ("Requires: ");
     }
-  st = message ("%s: %s %s %s",
+  st = message ("%q: %q %q %q",
                type,
                constraintExpr_print (c->lexpr),
                arithType_print(c->ar),
@@ -495,7 +813,30 @@ cstring  constraint_print (constraint c) /*@*/
   return st;
 }
 
-constraint constraint_doSRefFixBaseParam (constraint precondition,
+cstring  constraint_printOr (constraint c) /*@*/
+{
+  cstring ret;
+  constraint temp;
+
+  ret = cstring_undefined;
+  temp = c;
+
+  ret = cstring_concatFree (ret, constraint_print(temp) );
+
+  temp = temp->or;
+  
+  while ( constraint_isDefined(temp) ) 
+    {
+      ret = cstring_concatFree (ret, cstring_makeLiteral (" OR ") );
+      ret = cstring_concatFree (ret, constraint_print(temp) );
+      temp = temp->or;
+    }
+
+  return ret;
+
+}
+
+/*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
                                                   exprNodeList arglist)
 {
   precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
@@ -516,7 +857,7 @@ constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
   return postcondition;
 }
 
-constraint constraint_doSRefFixConstraintParam (constraint precondition,
+/*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
                                                   exprNodeList arglist)
 {
 
@@ -524,6 +865,7 @@ constraint constraint_doSRefFixConstraintParam (constraint precondition,
   precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
   precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
 
+  precondition->fcnPre = FALSE;
   return precondition;
 }
 
@@ -540,11 +882,43 @@ constraint constraint_doSRefFixConstraintParam (constraint precondition,
 //   return FALSE;
 // }
 
-constraint constraint_preserveOrig (constraint c)
+constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
 {
-  c->orig = constraint_copy (c);
+
+  DPRINTF( (message("Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
+  
+  if (c->orig == constraint_undefined)
+    c->orig = constraint_copy (c);
+
+  else if (c->orig->fcnPre)
+    {
+      constraint temp;
+      
+      temp = c->orig;
+      
+      /* avoid infinite loop */
+      c->orig = NULL;
+      c->orig = constraint_copy (c);
+      if (c->orig->orig == NULL)
+       c->orig->orig = temp;
+      else
+       llcontbug((message("Expected c->orig->orig to be null" ) ));
+    }
+  else
+    {
+      DPRINTF( (message("Not changing constraint") ));
+    }
+  
+  DPRINTF( (message("After Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
+
   return c;
 }
 /*@=fcnuse*/
 /*@=assignexpose*/
 /*@=czechfcns@*/
+
+constraint constraint_togglePost (/*@returned@*/ constraint c)
+{
+  c->post = !c->post;
+  return c;
+}
This page took 0.085127 seconds and 4 git commands to generate.