]>
Commit | Line | Data |
---|---|---|
92c4a786 | 1 | #ifndef __constraint_h__ |
bf92e32c | 2 | |
92c4a786 | 3 | #define __constraint_h__ |
bf92e32c | 4 | |
d0e5b01f | 5 | typedef enum |
6 | { | |
7 | LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE | |
8 | } | |
9 | arithType; | |
10 | ||
bf92e32c | 11 | //abst_typedef struct constr_ * constr; |
4cccc6ad | 12 | |
13 | ||
14 | struct _constraint { | |
bf92e32c | 15 | constraint orig; |
361091cc | 16 | constraintExpr lexpr; |
4cccc6ad | 17 | arithType ar; |
361091cc | 18 | constraintExpr expr; |
4cccc6ad | 19 | bool post; |
d0e5b01f | 20 | } ; |
21 | ||
92c4a786 | 22 | abst_typedef struct _constraintTerm * constraintTerm; |
23 | ||
4cccc6ad | 24 | //constraint constraint_create (exprNode e1, exprNode e2, arithType restriction, constraintType kind); |
25 | ||
26 | constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2); | |
27 | ||
28 | constraint constraint_makeInc_Op (exprNode p_e1); | |
29 | ||
30 | /*@i22*/ | |
31 | /*@-czechfcns*/ | |
32 | bool constraint_resolve (/*@unused@*/ constraint c); | |
33 | ||
34 | /*@out@*/ constraintTerm new_constraintTermExpr (void); | |
35 | constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e); | |
36 | ||
37 | constraintTerm intLit_makeConstraintTerm (int p_i); | |
38 | ||
39 | /*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term) | |
361091cc | 40 | /*@post:isnull result->expr@*/ |
4cccc6ad | 41 | /*@post:notnull result->t1@*/ |
361091cc | 42 | /*@defines result->expr, result->t1, result->c1@, result->op*/; |
4cccc6ad | 43 | |
44 | constraintExpr makeConstraintExprIntlit (int p_i); | |
45 | ||
46 | /*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind); | |
47 | ||
48 | constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind); | |
49 | ||
50 | constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index); | |
51 | ||
52 | constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint); | |
53 | ||
54 | constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint); | |
55 | ||
56 | constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc p_sequencePoint); | |
4cccc6ad | 57 | |
361091cc | 58 | constraint constraint_copy (constraint c); |
4cccc6ad | 59 | |
60 | constraintExpr makePostOpInc (exprNode t1); | |
61 | ||
62 | ||
63 | ||
361091cc | 64 | cstring constraintTerm_print (constraintTerm term); |
4cccc6ad | 65 | |
361091cc | 66 | cstring arithType_print (arithType ar); |
4cccc6ad | 67 | |
361091cc | 68 | cstring constraintExpr_print (constraintExpr ex); |
92c4a786 | 69 | fileloc constraint_getFileloc (constraint c); |
361091cc | 70 | cstring constraint_print (constraint c); |
4cccc6ad | 71 | /*@=czechfcns*/ |
361091cc | 72 | #warning take this out |
4cccc6ad | 73 | #include "constraintList.h" |
d0e5b01f | 74 | |
92c4a786 | 75 | #include "constraintExpr.h" |
361091cc | 76 | #include "constraintTerm.h" |
d0e5b01f | 77 | |
92c4a786 | 78 | #endif |
d0e5b01f | 79 |