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 a50051a5578fbe031bc1fbaed4ea7ccc91817ed5..58b8de6d665a0413c41eb46308aa5d1ebe8dfc23 100644 (file)
--- a/src/Headers/constraint.h
+++ b/src/Headers/constraint.h
@@ -17,6 +17,7 @@ struct _constraint {
   arithType       ar;
   constraintExpr  expr;
   bool post;
+  exprNode generatingExpr;
 } ;
 
 abst_typedef struct _constraintTerm * constraintTerm;
@@ -71,14 +72,14 @@ fileloc constraint_getFileloc (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);
 
-constraint constraint_preserveOrig (constraint c);
-constraint constraint_doSRefFixBaseParam (constraint precondition,
+/*@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);
@@ -91,7 +92,7 @@ constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, file
 
 /*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,
@@ -103,6 +104,23 @@ 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
 #include "constraintList.h"
@@ -110,5 +128,7 @@ constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer);
 #include "constraintExpr.h"
 #include "constraintTerm.h"
 #include "constraintResolve.h"
+#include "constraintOutput.h"
+
 #endif