-typedef union constraintTermValue_
-{
- exprNode expr;
- sRef sref;
- int intlit;
-} constraintTermValue;
+#ifndef __constraint_h__
+
+#define __constraint_h__
typedef enum
{
- LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE
+ LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE,
}
arithType;
-typedef enum
-{
- BUFFSIZE, STRINGLEN, VALUE, CALLSAFE,
- MAXSET, MINSET, MAXREAD, MINREAD,
- NULLTERMINATED,
- INCOP,
- UNDEFINED
-}
-constraintType;
+struct s_constraint {
+ arithType ar;
+ constraint orig;
+ constraint or;
+ bool fcnPre;
+ constraintExpr lexpr;
+ constraintExpr expr;
+ bool post;
+ /*@exposed@*/ /*@dependent@*/ exprNode generatingExpr;
+} ;
-typedef enum
-{
- PLUS,
- MINUS
-}
-constraintExprOp;
+/*@constant null constraint constraint_undefined; @*/
+# define constraint_undefined ((constraint)NULL)
-typedef enum
-{
-EXPRNODE, SREF,
-INTLITERAL
-} constraintTermType;
+extern /*@falsewhennull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ;
+extern /*@unused@*/ /*@nullwhentrue@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ;
+extern /*@nullwhentrue@*/ /*@unused@*/ bool constraint_isError (constraint p_e) /*@*/ ;
+# define constraint_isDefined(e) ((e) != constraint_undefined)
+# define constraint_isUndefined(e) ((e) == constraint_undefined)
+# define constraint_isError(e) ((e) == constraint_undefined)
-struct _constraintTerm {
- constraintType constrType;
- fileloc loc;
- constraintTermValue value;
- constraintTermType kind;
-};
+extern void constraint_free (/*@only@*/ constraint p_c);
-abst_typedef struct _constraintTerm * constraintTerm;
+/* constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant); */
-struct constraintExpr_ {
+/*@-czechfcns*/
- constraintTerm term;
- constraintExprOp op;
- struct constraintExpr_ * expr;
-};
-# define constraintExpr_undefined ((constraintExpr)NULL)
+extern constraint
+constraint_makeReadSafeExprNode (/*@observer@*/ exprNode p_po,
+ /*@observer@*/ exprNode p_ind);
-typedef struct constraintExpr_ * constraintExpr;
-abst_typedef struct constr_ * constr;
+extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (/*@observer@*/ exprNode p_po,
+ /*@observer@*/ exprNode p_ind);
+extern /*@only@*/ constraint constraint_makeReadSafeInt (/*@observer@*/ exprNode p_t1, int p_index);
-struct _constraint {
- constraintExpr lexpr;
- arithType ar;
- constraintExpr expr;
- bool post;
-} ;
+extern /*@only@*/ constraint
+constraint_makeEnsureMaxReadAtLeast (/*@observer@*/ exprNode p_t1,
+ /*@observer@*/ exprNode p_t2, fileloc p_sequencePoint);
-#define max_constraints 100
+extern void constraint_overWrite (constraint p_c1, /*@observer@*/ constraint p_c2)
+ /*@modifies p_c1 @*/;
-//constraint constraint_create (exprNode e1, exprNode e2, arithType restriction, constraintType kind);
+extern /*@only@*/ constraint constraint_copy (/*@temp@*/ constraint p_c);
-constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2);
+extern bool fileloc_closer (/*@observer@*/ fileloc p_loc1,
+ /*@observer@*/ fileloc p_loc2,
+ /*@observer@*/ fileloc p_loc3) /*@*/;
-constraint constraint_makeInc_Op (exprNode p_e1);
+extern /*@only@*/ cstring arithType_print (arithType p_ar) /*@*/;
-/*@i22*/
-/*@-czechfcns*/
-bool constraint_resolve (/*@unused@*/ constraint c);
-
-/*@out@*/ constraintTerm new_constraintTermExpr (void);
-constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e);
+extern /*@only@*/ fileloc constraint_getFileloc (constraint p_c);
+
+extern /*@only@*/ cstring constraint_unparse (/*@temp@*/ constraint p_c) /*@*/;
+extern /*@only@*/ cstring constraint_unparseOr (/*@temp@*/ constraint p_c) /*@*/ ;
+extern /*@only@*/ cstring constraint_unparseDetailed (constraint p_c) /*@*/ ;
+
+extern /*@only@*/ constraint
+constraint_makeWriteSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_po, int p_ind);
-constraintTerm intLit_makeConstraintTerm (int p_i);
+extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode p_dst, exprNode p_src) /*@modifies p_dst @*/;
-/*@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_makeEnsureEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
-/*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind);
+extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (/*@dependent@*/ /*@observer@*/ exprNode p_e, fileloc p_sequencePoint);
-constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind);
+extern constraint constraint_preserveOrig (/*@returned@*/ constraint p_c) /*@modifies p_c @*/;
+extern /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint p_precondition,
+ exprNodeList p_arglist);
+extern /*@only@*/ constraint constraint_makeEnsureLessThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
-constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index);
+extern /*@only@*/ constraint constraint_makeEnsureGreaterThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
+extern /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
-constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint);
+/*drl add 11/28/2000 */
+extern /*@only@*/ constraint constraint_makeSRefWriteSafeInt (sRef p_s, int p_ind);
+extern /*@unused@*/ /*@only@*/ constraint constraint_makeSRefReadSafeInt (sRef p_s, int p_ind);
+/*drl add 11/26/2000 */
+extern void constraint_printError (/*@observer@*/ /*@temp@*/ constraint p_c, /*@temp@*/ /*@observer@*/ fileloc p_loc);
-constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint);
+extern /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint p_precondition,
+ /*@temp@*/ /*@observer@*/ exprNodeList p_arglist);
-constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc p_sequencePoint);
-cstring constraintType_print (constraintType c1);
+extern /*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef p_s, long int p_size);
-constraint constraint_copy (constraint c);
+extern /*@only@*/ constraint constraint_doFixResult (constraint p_postcondition, /*@dependent@*/ /*@observer@*/ exprNode p_fcnCall);
-constraintExpr makePostOpInc (exprNode t1);
+extern /*@only@*/ constraint constraint_makeEnsureLteMaxRead(/*@dependent@*/ /*@observer@*/ exprNode p_index, /*@dependent@*/ /*@observer@*/ exprNode p_buffer);
+extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (/*@dependent@*/ /*@observer@*/ exprNode p_e, fileloc p_sequencePoint);
+extern bool constraint_search (constraint p_c, constraintExpr p_old);
-cstring constraintTerm_print (constraintTerm term);
+extern /*@only@*/ constraint makeConstraintParse3 (constraintExpr p_l, lltok p_relOp, constraintExpr p_r);
-cstring arithType_print (arithType ar);
+extern constraint constraint_addGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@exposed@*/ exprNode p_e);
-cstring constraintExpr_print (constraintExpr ex);
+extern bool constraint_hasMaxSet(constraint p_c);
-cstring constraint_print (constraint c);
+/*from constraintGenreation.c*/
+extern void exprNode_exprTraverse (exprNode p_e, bool p_definatelv, bool p_definaterv, /*@temp@*/ /*@observer@*/ fileloc p_sequencePoint);
+
+extern /*@only@*/ constraintList
+exprNode_traverseRequiresConstraints (exprNode p_e);
+
+extern /*@only@*/ constraintList
+exprNode_traverseEnsuresConstraints (exprNode p_e);
+
+extern constraint constraint_togglePost (/*@returned@*/ constraint p_c);
+extern bool constraint_same (constraint p_c1, constraint p_c2) ;
+extern void constraint_printErrorPostCondition (constraint p_c, fileloc p_loc) ;
+
+extern cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint p_c) /*@*/; /*drl add 8-11-001*/
+
+extern constraint constraint_setFcnPre (/*@returned@*/ constraint p_c) ;
+extern constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@observer@*/ exprNode p_e) ;
+
+extern bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode p_e) ;
+constraint constraint_togglePostOrig (/*@returned@*/ constraint p_c);
+
+bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint p_c);
+
+constraint constraint_makeAddAssign (/*@dependent@*/ /*@observer@*/ exprNode p_e, /*@dependent@*/ /*@observer@*/ exprNode p_f, fileloc p_sequencePoint);
+
+constraint constraint_makeSubtractAssign (/*@dependent@*/ /*@observer@*/ exprNode p_e, /*@dependent@*/ /*@observer@*/ exprNode p_f, fileloc p_sequencePoint);
+
+/*@only@*/ constraint constraint_undump (FILE * p_f);
+
+void constraint_dump (/*@observer@*/ constraint p_c, FILE * p_f);
+
+extern void exprNode_forLoopHeuristics( /*@dependent@*/ exprNode p_e, /*@dependent@*/ exprNode p_forPred, /*@dependent@*/ exprNode p_forBody);
+
+int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * p_c1, /*@observer@*/ /*@temp@*/ const constraint * p_c2) /*@*/;
+
+bool constraint_isPost (/*@observer@*/ /*@temp@*/ constraint p_c);
+
+bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint p_c);
+
+void exprNode_findValue( exprNode p_e);
+
+/*drl 1/6/2001: I didn't think these functions were solid enough to include in the stable release of splint.*/
+/*drl added 12/30/01 */
+/* extern / *@only@* / constraint constraint_doSRefFixInvarConstraint(constraint p_invar, sRef p_s, ctype p_ct ); */
+
+/*drl added 12/19 */
+bool constraint_isConstantOnly (constraint p_c);
/*@=czechfcns*/
-#warning take this out
-#include "constraintList.h"
+/* drl possible problem : warning take this out */
+
+#include "constraintResolve.h"
+#include "constraintOutput.h"
-#include "constraintTerm.h"
+#else
+#error Multiple include
+#endif