Prewinter break editing commit.

[splint.git] / src / Headers / constraint.h

diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h
index 4336289c3a57d0245736ac0d5e47a964c5f01fe9..b3379b133903f7629a8ef46feb98014f58ee36fb 100644 (file)
--- a/src/Headers/constraint.h
+++ b/src/Headers/constraint.h
@@ -23,6 +23,10 @@ abst_typedef struct _constraintTerm * constraintTerm;
 
 //constraint constraint_create (exprNode e1, exprNode e2,  arithType restriction, constraintType kind);
 
+
+constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant);
+
+
 constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2);
 
 constraint constraint_makeInc_Op (exprNode p_e1);
@@ -61,13 +65,13 @@ constraintExpr makePostOpInc (exprNode t1);
 
 
 bool fileloc_closer (fileloc  loc1, fileloc  loc2, fileloc  loc3);
-cstring constraintTerm_print (constraintTerm term);
+cstring constraintTerm_print (constraintTerm term) /*@*/;
 
-cstring arithType_print (arithType ar);
+cstring arithType_print (arithType ar) /*@*/;
 
-cstring constraintExpr_print (constraintExpr ex);
+cstring constraintExpr_print (constraintExpr ex) /*@*/;
 fileloc constraint_getFileloc (constraint c);
-cstring constraint_print (constraint c);
+cstring constraint_print (constraint c) /*@*/;
 constraint constraint_makeWriteSafeInt (exprNode po, int ind);
 
 exprNode exprNode_copyConstraints (exprNode dst, exprNode src);
@@ -76,6 +80,21 @@ constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequenc
 
 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint);
 
+constraint constraint_preserveOrig (constraint c);
+constraint constraint_doSRefFixBaseParam (constraint precondition,
+                                                  exprNodeList arglist);
+
+cstring  constraint_printDetailed (constraint c);
+
+constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint);
+
+constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
+constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint);
+constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
+
+/*drl add 11/28/2000 */
+constraint constraint_makeSRefWriteSafeInt (sRef s, int ind);
+
 /*@=czechfcns*/
 #warning take this out
 #include "constraintList.h"