struct _constraint {
constraint orig;
+ constraint or;
constraintExpr lexpr;
arithType ar;
constraintExpr expr;
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);
/*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,
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"
#include "constraintExpr.h"
#include "constraintTerm.h"
#include "constraintResolve.h"
+#include "constraintOutput.h"
+
#endif