]> andersk Git - splint.git/blobdiff - src/constraint.c
Fixed /*@i@*/ warning in splintme
[splint.git] / src / constraint.c
index fe7b638372d1def9a463154377861c5cdfeb932d..3706574599ec1cf2e2881a2934b392d19973cd73 100644 (file)
 
 /* #define DEBUGPRINT 1 */
 
-# include <ctype.h> /* for isdigit */
 # include "splintMacros.nf"
 # include "basic.h"
 # include "cgrammar.h"
 # include "cgrammar_tokens.h"
-
 # include "exprChecks.h"
 # include "exprNodeSList.h"
 
-
-static /*@only@*/ cstring constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
+static /*@only@*/ cstring 
+constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
 
 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
      /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/
@@ -50,39 +48,6 @@ advanceField (char **s)
   reader_checkChar (s, '@');
 }
 
-# if 0
-static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)    
-{
-  char *t;
-  int c;
-  constraint ret;
-  ret = constraint_makeNew ();
-  llassert (constraintExpr_isDefined (l));
-      
-  ret->lexpr = constraintExpr_copy (l);
-
-
-  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);
-
-  ret->post = TRUE;
-  DPRINTF (("GENERATED CONSTRAINT:"));
-  DPRINTF ((message ("%s", constraint_unparse (ret))));
-  return ret;
-}
-# endif
-
 bool constraint_same (constraint c1, constraint c2)
 {
   llassert (c1 != NULL);
@@ -158,7 +123,6 @@ constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
   ret->generatingExpr = c->generatingExpr;
   /*@=assignexpose@*/
   
-  /*@i33 fix this*/
   if (c->orig != NULL)
     ret->orig = constraint_copy (c->orig);
   else
@@ -174,7 +138,7 @@ constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
   return ret;
 }
 
-/*like copy expect it doesn't allocate memory for the constraint*/
+/*like copy except it doesn't allocate memory for the constraint*/
 
 void constraint_overWrite (constraint c1, constraint c2) 
 {
@@ -201,7 +165,6 @@ void constraint_overWrite (constraint c1, constraint c2)
   else
     c1->orig = NULL;
 
-  /*@i33 make sure that the or is freed correctly*/
   if (c1->or != NULL)
     constraint_free (c1->or);
 
@@ -348,7 +311,6 @@ constraint constraint_makeReadSafeExprNode (exprNode po, exprNode ind)
 constraint constraint_makeWriteSafeInt (   exprNode po, int ind)
 {
   constraint ret = constraint_makeNew ();
-
  
   ret->lexpr =constraintExpr_makeMaxSetExpr (po);
   ret->ar = GTE;
@@ -363,7 +325,6 @@ constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
  ret->ar = EQ;
  ret->expr =  constraintExpr_makeIntLiteral ((int)size);
  ret->post = TRUE;
- /*@i1*/
  return ret;
 }
 
@@ -376,7 +337,6 @@ constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
   ret->ar = GTE;
   ret->expr =  constraintExpr_makeIntLiteral (ind);
   ret->post = TRUE;
-  /*@i1*/
   return ret;
 }
 
This page took 0.031202 seconds and 4 git commands to generate.