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@*/
bool fileloc_closer (fileloc loc1, fileloc loc2, fileloc loc3);
-cstring constraintTerm_print (constraintTerm term) /*@*/;
+
cstring arithType_print (arithType ar) /*@*/;
-cstring constraintExpr_print (constraintExpr ex) /*@*/;
+
fileloc constraint_getFileloc (constraint c);
cstring constraint_print (constraint c) /*@*/;
constraint constraint_makeWriteSafeInt (exprNode po, int ind);
/*drl add 11/28/2000 */
constraint constraint_makeSRefWriteSafeInt (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);
+
/*@=czechfcns*/
-#warning take this out
+//#warning take this out
#include "constraintList.h"
#include "constraintExpr.h"