1 #ifndef __constraint_h__
3 #define __constraint_h__
7 LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE
11 //abst_typedef struct constr_ * constr;
22 abst_typedef struct _constraintTerm * constraintTerm;
24 //constraint constraint_create (exprNode e1, exprNode e2, arithType restriction, constraintType kind);
27 constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant);
30 constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2);
32 constraint constraint_makeInc_Op (exprNode p_e1);
36 bool constraint_resolve (/*@unused@*/ constraint c);
38 /*@out@*/ constraintTerm new_constraintTermExpr (void);
39 constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e);
41 constraintTerm intLit_makeConstraintTerm (int p_i);
43 /*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term)
44 /*@post:isnull result->expr@*/
45 /*@post:notnull result->t1@*/
46 /*@defines result->expr, result->t1, result->c1@, result->op*/;
48 constraintExpr makeConstraintExprIntlit (int p_i);
50 /*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind);
52 constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind);
54 constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index);
56 constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint);
58 constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint);
60 constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc p_sequencePoint);
61 void constraint_overWrite (constraint c1, constraint c2);
62 constraint constraint_copy (constraint c);
64 constraintExpr makePostOpInc (exprNode t1);
67 bool fileloc_closer (fileloc loc1, fileloc loc2, fileloc loc3);
68 cstring constraintTerm_print (constraintTerm term) /*@*/;
70 cstring arithType_print (arithType ar) /*@*/;
72 cstring constraintExpr_print (constraintExpr ex) /*@*/;
73 fileloc constraint_getFileloc (constraint c);
74 cstring constraint_print (constraint c) /*@*/;
75 constraint constraint_makeWriteSafeInt (exprNode po, int ind);
77 exprNode exprNode_copyConstraints (exprNode dst, exprNode src);
79 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
81 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint);
83 constraint constraint_preserveOrig (constraint c);
84 constraint constraint_doSRefFixBaseParam (constraint precondition,
85 exprNodeList arglist);
87 cstring constraint_printDetailed (constraint c);
89 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint);
91 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
92 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint);
93 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
95 /*drl add 11/28/2000 */
96 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind);
99 #warning take this out
100 #include "constraintList.h"
102 #include "constraintExpr.h"
103 #include "constraintTerm.h"
104 #include "constraintResolve.h"