]>
Commit | Line | Data |
---|---|---|
4cccc6ad | 1 | /* |
2 | ** constraintList.c | |
3 | */ | |
4 | ||
5 | # include <ctype.h> /* for isdigit */ | |
6 | # include "lclintMacros.nf" | |
7 | # include "basic.h" | |
8 | # include "cgrammar.h" | |
9 | # include "cgrammar_tokens.h" | |
10 | ||
11 | # include "exprChecks.h" | |
12 | # include "aliasChecks.h" | |
13 | # include "exprNodeSList.h" | |
14 | # include "exprData.i" | |
15 | ||
16 | /*@i33*/ | |
17 | /*@-fcnuse*/ | |
18 | /*@-assignexpose*/ | |
19 | ||
361091cc | 20 | /*@notnull@*/ |
21 | /*@special@*/ constraint constraint_makeNew (void) | |
22 | /*@post:isnull result->term, result->expr, result->constrType@*/ | |
23 | /*@defines result->ar, result->post@*/; | |
24 | ||
4cccc6ad | 25 | constraint constraint_copy (constraint c) |
26 | { | |
27 | constraint ret; | |
28 | ret = constraint_makeNew(); | |
bf92e32c | 29 | ret->lexpr = constraintExpr_copy (c->lexpr); |
4cccc6ad | 30 | ret->ar = c->ar; |
bf92e32c | 31 | ret->expr = constraintExpr_copy (c->expr); |
4cccc6ad | 32 | ret->post = c->post; |
bf92e32c | 33 | /*@i33 fix this*/ |
34 | if (c->orig != NULL) | |
35 | ret->orig = constraint_copy (c->orig); | |
36 | else | |
37 | ret->orig = NULL; | |
4cccc6ad | 38 | return ret; |
39 | } | |
40 | ||
92c4a786 | 41 | /*like copy expect it doesn't allocate memory for the constraint*/ |
42 | ||
43 | void constraint_overWrite (constraint c1, constraint c2) | |
44 | { | |
45 | c1->lexpr = constraintExpr_copy (c2->lexpr); | |
46 | c1->ar = c2->ar; | |
47 | c1->expr = constraintExpr_copy (c2->expr); | |
48 | c1->post = c2->post; | |
49 | /*@i33 fix this*/ | |
50 | if (c2->orig != NULL) | |
51 | c1->orig = constraint_copy (c2->orig); | |
52 | else | |
53 | c1->orig = NULL; | |
54 | ||
55 | } | |
56 | ||
4cccc6ad | 57 | bool constraint_resolve (/*@unused@*/ constraint c) |
58 | { | |
59 | return FALSE; | |
60 | } | |
61 | ||
62 | /*@notnull@*/ | |
63 | /*@special@*/ constraint constraint_makeNew (void) | |
361091cc | 64 | /*@post:isnull result->term, result->expr, result->constrType@*/ |
4cccc6ad | 65 | /*@defines result->ar, result->post@*/ |
66 | { | |
67 | constraint ret; | |
68 | ret = dmalloc(sizeof (*ret) ); | |
361091cc | 69 | ret->lexpr = NULL; |
70 | ret->expr = NULL; | |
4cccc6ad | 71 | ret->ar = LT; |
72 | ret->post = FALSE; | |
bf92e32c | 73 | ret->orig = NULL; |
4cccc6ad | 74 | /*@i23*/return ret; |
75 | } | |
4cccc6ad | 76 | |
92c4a786 | 77 | fileloc constraint_getFileloc (constraint c) |
361091cc | 78 | { |
92c4a786 | 79 | return (constraintExpr_getFileloc (c->lexpr) ); |
4cccc6ad | 80 | |
4cccc6ad | 81 | |
4cccc6ad | 82 | } |
83 | ||
361091cc | 84 | constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind) |
85 | { | |
86 | constraint ret = constraint_makeNew(); | |
87 | // constraintTerm term; | |
88 | po = exprNode_fakeCopy(po); | |
89 | ind = exprNode_fakeCopy(ind); | |
90 | ret->lexpr = constraintExpr_makeMaxReadExpr(po); | |
91 | ret->ar = GTE; | |
92 | ret->expr = constraintExpr_makeValueExpr (ind); | |
93 | return ret; | |
94 | } | |
4cccc6ad | 95 | |
361091cc | 96 | constraint constraint_makeWriteSafeInt (exprNode po, int ind) |
4cccc6ad | 97 | { |
98 | constraint ret = constraint_makeNew(); | |
92c4a786 | 99 | |
361091cc | 100 | |
101 | ret->lexpr =constraintExpr_makeMaxSetExpr(po); | |
4cccc6ad | 102 | ret->ar = GTE; |
361091cc | 103 | ret->expr = constraintExpr_makeValueInt (ind); |
104 | /*@i1*/return ret; | |
4cccc6ad | 105 | } |
92c4a786 | 106 | |
107 | constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind) | |
108 | { | |
109 | constraint ret = constraint_makeNew(); | |
110 | ||
111 | ||
112 | ret->lexpr =constraintExpr_makeMaxSetExpr(po); | |
113 | ret->ar = GTE; | |
114 | ret->expr = constraintExpr_makeValueExpr (ind); | |
115 | /*@i1*/return ret; | |
116 | } | |
117 | ||
361091cc | 118 | constraint constraint_makeReadSafeInt ( exprNode po, int ind) |
119 | { | |
120 | constraint ret = constraint_makeNew(); | |
4cccc6ad | 121 | |
361091cc | 122 | po = exprNode_fakeCopy(po); |
123 | ||
124 | ret->lexpr = constraintExpr_makeMaxReadExpr(po); | |
125 | ret->ar = GTE; | |
126 | ret->expr = constraintExpr_makeValueInt (ind); | |
127 | return ret; | |
128 | } | |
4cccc6ad | 129 | |
361091cc | 130 | constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint) |
4cccc6ad | 131 | { |
132 | constraint ret = constraint_makeNew(); | |
92c4a786 | 133 | |
4cccc6ad | 134 | |
361091cc | 135 | e1 = exprNode_fakeCopy (e1); |
4cccc6ad | 136 | t2 = exprNode_fakeCopy (t2); |
137 | ||
361091cc | 138 | ret = constraint_makeReadSafeExprNode(e1, t2); |
92c4a786 | 139 | |
140 | ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); | |
4cccc6ad | 141 | |
4cccc6ad | 142 | ret->post = TRUE; |
361091cc | 143 | |
92c4a786 | 144 | // fileloc_incColumn (ret->lexpr->term->loc); |
361091cc | 145 | return ret; |
4cccc6ad | 146 | } |
147 | ||
361091cc | 148 | |
754746a0 | 149 | /* make constraint ensures e1 == e2 */ |
150 | ||
151 | constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint) | |
152 | { | |
153 | constraint ret = constraint_makeNew(); | |
154 | exprNode e; | |
155 | ||
156 | e = exprNode_fakeCopy(e1); | |
157 | ret->lexpr = constraintExpr_makeValueExpr (e); | |
158 | ret->ar = EQ; | |
159 | ret->post = TRUE; | |
160 | e = exprNode_fakeCopy(e2); | |
161 | ret->expr = constraintExpr_makeValueExpr (e); | |
162 | ||
163 | ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); | |
164 | // fileloc_incColumn ( ret->lexpr->term->loc); | |
165 | // fileloc_incColumn ( ret->lexpr->term->loc); | |
166 | return ret; | |
167 | } | |
168 | ||
169 | ||
170 | exprNode exprNode_copyConstraints (exprNode dst, exprNode src) | |
171 | { | |
172 | dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints ); | |
173 | dst->requiresConstraints = constraintList_copy (src->requiresConstraints ); | |
174 | dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints ); | |
175 | dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints ); | |
176 | return dst; | |
177 | } | |
178 | ||
361091cc | 179 | constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint) |
4cccc6ad | 180 | { |
181 | constraint ret = constraint_makeNew(); | |
182 | //constraintTerm term; | |
92c4a786 | 183 | |
361091cc | 184 | e = exprNode_fakeCopy(e); |
bf92e32c | 185 | ret->lexpr = constraintExpr_makeValueExpr (e); |
4cccc6ad | 186 | ret->ar = EQ; |
187 | ret->post = TRUE; | |
92c4a786 | 188 | ret->expr = constraintExpr_makeValueExpr (e); |
189 | ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr); | |
4cccc6ad | 190 | |
754746a0 | 191 | ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); |
92c4a786 | 192 | // fileloc_incColumn ( ret->lexpr->term->loc); |
193 | // fileloc_incColumn ( ret->lexpr->term->loc); | |
361091cc | 194 | return ret; |
4cccc6ad | 195 | } |
361091cc | 196 | |
754746a0 | 197 | |
198 | ||
92c4a786 | 199 | // constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint) |
200 | // { | |
201 | // constraint ret = constraint_makeNew(); | |
202 | // //constraintTerm term; | |
4cccc6ad | 203 | |
92c4a786 | 204 | // e = exprNode_fakeCopy(e); |
205 | // ret->lexpr = constraintExpr_makeMaxReadExpr(e); | |
206 | // ret->ar = EQ; | |
207 | // ret->post = TRUE; | |
208 | // ret->expr = constraintExpr_makeIncConstraintExpr (e); | |
209 | // ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint); | |
210 | // return ret; | |
211 | // } | |
4cccc6ad | 212 | |
361091cc | 213 | |
214 | cstring arithType_print (arithType ar) | |
4cccc6ad | 215 | { |
361091cc | 216 | cstring st = cstring_undefined; |
4cccc6ad | 217 | switch (ar) |
218 | { | |
219 | case LT: | |
361091cc | 220 | st = cstring_makeLiteral (" < "); |
221 | break; | |
4cccc6ad | 222 | case LTE: |
361091cc | 223 | st = cstring_makeLiteral (" <= "); |
224 | break; | |
4cccc6ad | 225 | case GT: |
361091cc | 226 | st = cstring_makeLiteral (" > "); |
227 | break; | |
4cccc6ad | 228 | case GTE: |
361091cc | 229 | st = cstring_makeLiteral (" >= "); |
230 | break; | |
4cccc6ad | 231 | case EQ: |
361091cc | 232 | st = cstring_makeLiteral (" == "); |
233 | break; | |
4cccc6ad | 234 | case NONNEGATIVE: |
361091cc | 235 | st = cstring_makeLiteral (" NONNEGATIVE "); |
236 | break; | |
4cccc6ad | 237 | case POSITIVE: |
361091cc | 238 | st = cstring_makeLiteral (" POSITIVE "); |
239 | break; | |
4cccc6ad | 240 | default: |
241 | llassert(FALSE); | |
361091cc | 242 | break; |
4cccc6ad | 243 | } |
361091cc | 244 | return st; |
4cccc6ad | 245 | } |
246 | ||
4cccc6ad | 247 | |
bf92e32c | 248 | cstring constraint_printDetailed (constraint c) |
249 | { | |
250 | cstring st = cstring_undefined; | |
251 | ||
252 | if (!c->post) | |
253 | { | |
254 | ||
255 | st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisy %s", constraint_print (c), constraint_print(c->orig) ); | |
256 | } | |
257 | else | |
258 | { | |
754746a0 | 259 | st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) ); |
bf92e32c | 260 | } |
261 | return st; | |
262 | } | |
263 | ||
361091cc | 264 | cstring constraint_print (constraint c) |
4cccc6ad | 265 | { |
361091cc | 266 | cstring st = cstring_undefined; |
267 | cstring type = cstring_undefined; | |
268 | llassert (c); | |
4cccc6ad | 269 | if (c->post) |
270 | { | |
361091cc | 271 | type = cstring_makeLiteral ("Ensures: "); |
4cccc6ad | 272 | } |
273 | else | |
274 | { | |
361091cc | 275 | type = cstring_makeLiteral ("Requires: "); |
4cccc6ad | 276 | } |
361091cc | 277 | st = message ("%s: %s %s %s", |
278 | type, | |
279 | constraintExpr_print (c->lexpr), | |
280 | arithType_print(c->ar), | |
281 | constraintExpr_print(c->expr) | |
282 | ); | |
283 | return st; | |
4cccc6ad | 284 | } |
285 | ||
92c4a786 | 286 | // bool constraint_hasTerm (constraint c, constraintTerm term) |
287 | // { | |
288 | // DPRINTF((message ("Constraint %s", constraint_print (c) ) ) ); | |
bf92e32c | 289 | |
92c4a786 | 290 | // if (constraintExpr_includesTerm (c->lexpr, term) ) |
291 | // return TRUE; | |
bf92e32c | 292 | |
92c4a786 | 293 | // if (constraintExpr_includesTerm (c->expr, term) ) |
294 | // return TRUE; | |
bf92e32c | 295 | |
92c4a786 | 296 | // return FALSE; |
297 | // } | |
bf92e32c | 298 | |
299 | constraint constraint_preserveOrig (constraint c) | |
300 | { | |
301 | c->orig = constraint_copy (c); | |
302 | return c; | |
303 | } | |
4cccc6ad | 304 | /*@=fcnuse*/ |
305 | /*@=assignexpose*/ | |
306 | /*@=czechfcns@*/ |