Fixed library dump support so that buffer constraint annotations are read and written...

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

diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h
index 9fd14fd3ff98a21d30959eb2372f7c692da796f2..9addd229444d66b135225cd828dd36568361ac2b 100644 (file)
--- a/src/Headers/constraint.h
+++ b/src/Headers/constraint.h
@@ -31,7 +31,7 @@ extern /*@truenull@*/ /*@unused@*/ bool constraint_isError (constraint p_e) /*@*
 # define constraint_isUndefined(e)      ((e) == constraint_undefined)
 # define constraint_isError(e)          ((e) == constraint_undefined)
 
-void constraint_free (/*@only@*/ /*@notnull@*/ constraint c);
+extern void constraint_free (/*@only@*/  constraint c);
 
 //constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant);
 
@@ -43,87 +43,95 @@ void constraint_free (/*@only@*/ /*@notnull@*/ constraint c);
 //     /*@post:notnull result->t1@*/
 //     /*@defines result->expr, result->t1, result->c1@, result->op*/;
      
-//constraintExpr makeConstraintExprIntlit (int p_i);
+extern /*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind);
 
-/*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind);
+extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind);
 
-/*@only@*/ constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind);
+extern /*@only@*/ constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index);
 
-/*@only@*/ constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index);
+extern /*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint);
 
-/*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint);
+extern void constraint_overWrite (constraint c1, /*@observer@*/ constraint c2) /*@modifies c1 @*/;
 
-void constraint_overWrite (constraint c1, /*@observer@*/ constraint c2) /*@modifies c1 @*/;
+extern /*@only@*/ constraint constraint_copy (/*@observer@*/ constraint c);
 
-/*@only@*/ constraint constraint_copy (/*@observer@*/ constraint c);
+extern bool fileloc_closer (/*@observer@*/ fileloc  loc1, /*@observer@*/ fileloc  loc2, /*@observer@*/ fileloc  loc3) /*@*/;
 
-//constraintExpr makePostOpInc (exprNode t1);
+extern /*@only@*/ cstring arithType_print (arithType ar) /*@*/;
 
+extern /*@only@*/ fileloc constraint_getFileloc (constraint c);
+extern /*@only@*/ cstring constraint_print (constraint c) /*@*/;
 
-bool fileloc_closer (/*@observer@*/ fileloc  loc1,/*@observer@*/ fileloc  loc2,/*@observer@*/ fileloc  loc3) /*@*/;
+extern /*@only@*/ constraint constraint_makeWriteSafeInt (exprNode po, int ind);
 
+extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src) /*@modifies dst @*/;
 
-/*@only@*/ cstring arithType_print (arithType ar) /*@*/;
+extern /*@only@*/ constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
 
+extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint);
 
-/*@only@*/fileloc constraint_getFileloc (constraint c);
-/*@only@*/ cstring constraint_print (constraint c) /*@*/;
+extern constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/;
+extern /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
+                                                           exprNodeList arglist);
+extern /*@only@*/ cstring  constraint_printDetailed (constraint c);
 
-/*@only@*/constraint constraint_makeWriteSafeInt (exprNode po, int ind);
+extern /*@only@*/ constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
 
-exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src) /*@modifies dst @*/;
+extern /*@only@*/ constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
 
-/*@only@*/ constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
-
-/*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint);
+/*drl add 11/28/2000 */
+extern /*@only@*/ constraint constraint_makeSRefWriteSafeInt (sRef s, int ind);
+extern /*@unused@*/ /*@only@*/ constraint constraint_makeSRefReadSafeInt (sRef s, int ind);
+/*drl add 11/26/2000 */
+extern void constraint_printError (/*@observer@*/ constraint c, /*@observer@*/ fileloc loc);
 
-constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/;
-/*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
-                                                    exprNodeList arglist);
+extern /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
+                                                                 exprNodeList arglist);
 
-/*@only@*/ cstring  constraint_printDetailed (constraint c);
+extern /*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef s, long int size);
 
-/*@only@*/ constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint);
+extern /*@only@*/ constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall);
 
-/*@only@*/ constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer);
 
-/*@only@*/ constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint);
-/*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
+extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint);
 
-/*drl add 11/28/2000 */
-/*@only@*/ constraint constraint_makeSRefWriteSafeInt (sRef s, int ind);
-/*@unused@*/ /*@only@*/ constraint constraint_makeSRefReadSafeInt (sRef s, int ind);
-/*drl add 11/26/2000 */
-void constraint_printError (/*@observer@*/ constraint c, /*@observer@*/ fileloc loc);
+extern bool constraint_search (constraint c, constraintExpr old);
 
-/*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
-                                               exprNodeList arglist);
+extern /*@only@*/ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r);
 
-/*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef s, long int size);
+extern constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e);
 
-/*@only@*/ constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall);
+extern bool constraint_hasMaxSet(constraint c);
 
-/*@only@*/ constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer);
+/*from constraintGenreation.c*/
+extern void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/  fileloc sequencePoint);
 
-/*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint);
+extern /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e);
+extern /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e);
 
-bool constraint_search (constraint c, constraintExpr old);
+extern constraint constraint_togglePost (/*@returned@*/ constraint c);
+extern bool constraint_same (constraint c1, constraint c2) ;
 
-/*@only@*/ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r);
+/*@only@*/ cstring  constraint_printOr (constraint c) /*@*/;
+extern void constraint_printErrorPostCondition (constraint p_c, fileloc p_loc) ;
+extern constraint constraint_setFcnPre (/*@returned@*/ constraint p_c) ;
+extern constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint p_c, exprNode p_e) ;
 
-constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e);
+extern bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode p_e) ;
+constraint constraint_togglePostOrig (/*@returned@*/ constraint c);
 
-bool constraint_hasMaxSet(constraint c);
+bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c);
 
-/*from constraintGenreation.c*/
-void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/  fileloc sequencePoint);
+constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint);
 
-/*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e);
-/*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e);
+constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint);
 
-constraint constraint_togglePost (/*@returned@*/ constraint c);
+/*@only@*/ constraint constraint_undump (FILE *f);
 
-/*@only@*/ cstring  constraint_printOr (constraint c) /*@*/;
+void constraint_dump (/*@observer@*/ constraint c,  FILE *f);
 
 /*@=czechfcns*/
 //#warning take this out