Added (limited) support for implicit annotations.

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

diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h
index 4336289c3a57d0245736ac0d5e47a964c5f01fe9..58b8de6d665a0413c41eb46308aa5d1ebe8dfc23 100644 (file)
--- a/src/Headers/constraint.h
+++ b/src/Headers/constraint.h
@@ -17,12 +17,17 @@ struct _constraint {
   arithType       ar;
   constraintExpr  expr;
   bool post;
+  exprNode generatingExpr;
 } ;
 
 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);
@@ -32,9 +37,6 @@ constraint constraint_makeInc_Op (exprNode p_e1);
 bool constraint_resolve (/*@unused@*/ constraint c);
      
 /*@out@*/ constraintTerm new_constraintTermExpr (void);
-constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e);
-
-constraintTerm intLit_makeConstraintTerm (int p_i);
 
 /*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term)
  /*@post:isnull result->expr@*/
@@ -61,27 +63,72 @@ constraintExpr makePostOpInc (exprNode t1);
 
 
 bool fileloc_closer (fileloc  loc1, fileloc  loc2, fileloc  loc3);
-cstring constraintTerm_print (constraintTerm term);
 
-cstring arithType_print (arithType ar);
 
-cstring constraintExpr_print (constraintExpr ex);
+cstring arithType_print (arithType ar) /*@*/;
+
+
 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);
+exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src);
 
 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
 
 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint);
 
+/*@only@*/ constraint constraint_preserveOrig (/*@returned@*/ /*@only@*/ constraint c) /*@modifies c @*/;
+/*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ 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);
+constraint constraint_makeSRefReadSafeInt (sRef s, int ind);
+/*drl add 11/26/2000 */
+void constraint_printError (constraint c, fileloc loc);
+constraint constraint_doSRefFixConstraintParam (constraint precondition,
+                                               exprNodeList arglist);
+
+constraint constraint_makeSRefSetBufferSize (sRef s, int size);
+
+constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall);
+
+constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer);
+
+constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint);
+bool constraint_search (constraint c, constraintExpr old);
+
+constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r);
+
+constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e);
+
+bool constraint_hasMaxSet(constraint c);
+
+/*from constraintGenreation.c*/
+bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  fileloc sequencePoint);
+
+constraintList exprNode_traversRequiresConstraints (exprNode e);
+constraintList exprNode_traversEnsuresConstraints (exprNode e);
+
+
+
 /*@=czechfcns*/
-#warning take this out
+//#warning take this out
 #include "constraintList.h"
 
 #include "constraintExpr.h"
 #include "constraintTerm.h"
 #include "constraintResolve.h"
+#include "constraintOutput.h"
+
 #endif