-/*from constraintGenreation.c*/
-bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint);
+/*@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);