+extern /*@only@*/ constraintList constraintList_doSRefFixBaseParam ( /*@observer@*/ constraintList preconditions, /*@observer@*/ exprNodeList arglist) /*@modifies preconditions@*/;
+
+extern constraintList constraintList_togglePost (/*@returned@*/ constraintList c) /*@modifies c@*/;
+
+extern /*@only@*/ constraintList constraintList_doSRefFixConstraintParam ( /*@only@*/ constraintList preconditions, /*@observer@*/ exprNodeList arglist) /*@modifies preconditions@*/;
+
+extern constraintList getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall) /*@*/;
+
+/*@only@*/ constraintList constraintList_doFixResult ( /*@only@*/ constraintList postconditions, /*@observer@*/ exprNode fcnCall) /*@modifies postconditions@*/;
+
+extern constraintList constraintList_addGeneratingExpr (/*@returned@*/ constraintList c, exprNode e) /*@modifies c@*/;
+extern /*@only@*/ constraintList constraintList_makeFixedArrayConstraints ( /*@observer@*/ sRefSet p_s) ;
+extern void constraintList_printErrorPostConditions (constraintList p_s, fileloc p_loc) ;
+extern void constraintList_printError (constraintList p_s, fileloc p_loc) ;
+
+void constraintList_dump (/*@observer@*/ constraintList c, FILE *f);
+
+/*@only@*/ constraintList constraintList_undump (FILE *f);
+
+