]>
Commit | Line | Data |
---|---|---|
4cccc6ad | 1 | typedef union constraintTermValue_ |
2 | { | |
bf92e32c | 3 | constraintExpr constrExpr; |
4cccc6ad | 4 | exprNode expr; |
5 | sRef sref; | |
6 | int intlit; | |
7 | } constraintTermValue; | |
8 | ||
bf92e32c | 9 | |
10 | typedef enum | |
11 | { | |
12 | EXPRNODE, SREF, | |
13 | CONSTRAINTEXPR, | |
14 | INTLITERAL | |
15 | } constraintTermType; | |
16 | ||
17 | ||
d0e5b01f | 18 | typedef enum |
19 | { | |
20 | LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE | |
21 | } | |
22 | arithType; | |
23 | ||
24 | typedef enum | |
25 | { | |
bf92e32c | 26 | //BUFFSIZE, STRINGLEN, |
27 | VALUE, CALLSAFE, | |
4cccc6ad | 28 | MAXSET, MINSET, MAXREAD, MINREAD, |
29 | NULLTERMINATED, | |
4cccc6ad | 30 | UNDEFINED |
d0e5b01f | 31 | } |
32 | constraintType; | |
33 | ||
4cccc6ad | 34 | typedef enum |
35 | { | |
36 | PLUS, | |
37 | MINUS | |
38 | } | |
39 | constraintExprOp; | |
40 | ||
41 | ||
4cccc6ad | 42 | struct _constraintTerm { |
361091cc | 43 | constraintType constrType; |
4cccc6ad | 44 | fileloc loc; |
45 | constraintTermValue value; | |
46 | constraintTermType kind; | |
47 | }; | |
d0e5b01f | 48 | |
4cccc6ad | 49 | abst_typedef struct _constraintTerm * constraintTerm; |
50 | ||
51 | struct constraintExpr_ { | |
361091cc | 52 | |
53 | constraintTerm term; | |
4cccc6ad | 54 | constraintExprOp op; |
361091cc | 55 | struct constraintExpr_ * expr; |
4cccc6ad | 56 | }; |
57 | # define constraintExpr_undefined ((constraintExpr)NULL) | |
58 | ||
bf92e32c | 59 | |
60 | //abst_typedef struct constr_ * constr; | |
4cccc6ad | 61 | |
62 | ||
63 | struct _constraint { | |
bf92e32c | 64 | constraint orig; |
361091cc | 65 | constraintExpr lexpr; |
4cccc6ad | 66 | arithType ar; |
361091cc | 67 | constraintExpr expr; |
4cccc6ad | 68 | bool post; |
d0e5b01f | 69 | } ; |
70 | ||
4cccc6ad | 71 | //constraint constraint_create (exprNode e1, exprNode e2, arithType restriction, constraintType kind); |
72 | ||
73 | constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2); | |
74 | ||
75 | constraint constraint_makeInc_Op (exprNode p_e1); | |
76 | ||
77 | /*@i22*/ | |
78 | /*@-czechfcns*/ | |
79 | bool constraint_resolve (/*@unused@*/ constraint c); | |
80 | ||
81 | /*@out@*/ constraintTerm new_constraintTermExpr (void); | |
82 | constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e); | |
83 | ||
84 | constraintTerm intLit_makeConstraintTerm (int p_i); | |
85 | ||
86 | /*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term) | |
361091cc | 87 | /*@post:isnull result->expr@*/ |
4cccc6ad | 88 | /*@post:notnull result->t1@*/ |
361091cc | 89 | /*@defines result->expr, result->t1, result->c1@, result->op*/; |
4cccc6ad | 90 | |
91 | constraintExpr makeConstraintExprIntlit (int p_i); | |
92 | ||
93 | /*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind); | |
94 | ||
95 | constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind); | |
96 | ||
97 | constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index); | |
98 | ||
99 | constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint); | |
100 | ||
101 | constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint); | |
102 | ||
103 | constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc p_sequencePoint); | |
361091cc | 104 | cstring constraintType_print (constraintType c1); |
4cccc6ad | 105 | |
361091cc | 106 | constraint constraint_copy (constraint c); |
4cccc6ad | 107 | |
108 | constraintExpr makePostOpInc (exprNode t1); | |
109 | ||
110 | ||
111 | ||
361091cc | 112 | cstring constraintTerm_print (constraintTerm term); |
4cccc6ad | 113 | |
361091cc | 114 | cstring arithType_print (arithType ar); |
4cccc6ad | 115 | |
361091cc | 116 | cstring constraintExpr_print (constraintExpr ex); |
4cccc6ad | 117 | |
361091cc | 118 | cstring constraint_print (constraint c); |
4cccc6ad | 119 | /*@=czechfcns*/ |
361091cc | 120 | #warning take this out |
4cccc6ad | 121 | #include "constraintList.h" |
d0e5b01f | 122 | |
361091cc | 123 | #include "constraintTerm.h" |
d0e5b01f | 124 | |
d0e5b01f | 125 | |
d0e5b01f | 126 |