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