}
arithType;
-//abst_typedef struct constr_ * constr;
-
-
struct _constraint {
constraint orig;
+ constraint or;
+ bool fcnPre;
constraintExpr lexpr;
arithType ar;
constraintExpr expr;
bool post;
+ /*@kept@*/ exprNode generatingExpr;
} ;
-abst_typedef struct _constraintTerm * constraintTerm;
+/*@constant null constraint constraint_undefined; @*/
+
+# define constraint_undefined ((constraint)NULL)
+
+extern /*@falsenull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ;
+extern /*@unused@*/ /*@truenull@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ;
+extern /*@truenull@*/ /*@unused@*/ bool constraint_isError (constraint p_e) /*@*/ ;
-//constraint constraint_create (exprNode e1, exprNode e2, arithType restriction, constraintType kind);
+# define constraint_isDefined(e) ((e) != constraint_undefined)
+# define constraint_isUndefined(e) ((e) == constraint_undefined)
+# define constraint_isError(e) ((e) == constraint_undefined)
-constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2);
+extern void constraint_free (/*@only@*/ constraint c);
-constraint constraint_makeInc_Op (exprNode p_e1);
+//constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant);
/*@i22*/
/*@-czechfcns*/
-bool constraint_resolve (/*@unused@*/ constraint c);
+
+///*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term)
+// /*@post:isnull result->expr@*/
+// /*@post:notnull result->t1@*/
+// /*@defines result->expr, result->t1, result->c1@, result->op*/;
-/*@out@*/ constraintTerm new_constraintTermExpr (void);
-constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e);
+extern /*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind);
-constraintTerm intLit_makeConstraintTerm (int p_i);
+extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind);
-/*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term)
- /*@post:isnull result->expr@*/
- /*@post:notnull result->t1@*/
- /*@defines result->expr, result->t1, result->c1@, result->op*/;
-
-constraintExpr makeConstraintExprIntlit (int p_i);
+extern /*@only@*/ constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index);
+
+extern /*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint);
+
+extern void constraint_overWrite (constraint c1, /*@observer@*/ constraint c2) /*@modifies c1 @*/;
+
+extern /*@only@*/ constraint constraint_copy (/*@observer@*/ constraint c);
+
+extern bool fileloc_closer (/*@observer@*/ fileloc loc1, /*@observer@*/ fileloc loc2, /*@observer@*/ fileloc loc3) /*@*/;
+
+extern /*@only@*/ cstring arithType_print (arithType ar) /*@*/;
+
+extern /*@only@*/ fileloc constraint_getFileloc (constraint c);
+extern /*@only@*/ cstring constraint_print (constraint c) /*@*/;
+
+extern /*@only@*/ constraint constraint_makeWriteSafeInt (exprNode po, int ind);
+
+extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src) /*@modifies dst @*/;
+
+extern /*@only@*/ constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
-/*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind);
+extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint);
-constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind);
+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);
-constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index);
+extern /*@only@*/ constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
-constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
-constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, 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_makeSideEffectPostIncrement (exprNode t1, fileloc p_sequencePoint);
+extern /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
+ exprNodeList arglist);
-constraint constraint_copy (constraint c);
+extern /*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef s, long int size);
-constraintExpr makePostOpInc (exprNode t1);
+extern /*@only@*/ constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall);
+extern /*@only@*/ constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer);
+extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint);
-cstring constraintTerm_print (constraintTerm term);
+extern bool constraint_search (constraint c, constraintExpr old);
-cstring arithType_print (arithType ar);
+extern /*@only@*/ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r);
+
+extern constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e);
+
+extern bool constraint_hasMaxSet(constraint c);
+
+/*from constraintGenreation.c*/
+extern void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ fileloc sequencePoint);
+
+extern /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e);
+extern /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e);
+
+extern constraint constraint_togglePost (/*@returned@*/ constraint c);
+extern bool constraint_same (constraint c1, constraint c2) ;
+
+/*@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) ;
+
+extern bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode p_e) ;
+constraint constraint_togglePostOrig (/*@returned@*/ constraint c);
+
+bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c);
+
+constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint);
+
+constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint);
+
+/*@only@*/ constraint constraint_undump (FILE *f);
+
+void constraint_dump (/*@observer@*/ constraint c, FILE *f);
-cstring constraintExpr_print (constraintExpr ex);
-fileloc constraint_getFileloc (constraint c);
-cstring constraint_print (constraint c);
/*@=czechfcns*/
-#warning take this out
-#include "constraintList.h"
+//#warning take this out
+
+#include "constraintResolve.h"
+#include "constraintOutput.h"
+
+#else
-#include "constraintExpr.h"
-#include "constraintTerm.h"
+#error Multiple include
#endif
andersk / splint.git / blobdiff