]>
Commit | Line | Data |
---|---|---|
616915dd | 1 | |
2 | /* | |
3 | ** constraintGeneration.c | |
4 | */ | |
5 | ||
6 | //#define DEBUGPRINT 1 | |
7 | ||
8 | # include <ctype.h> /* for isdigit */ | |
9 | # include "lclintMacros.nf" | |
10 | # include "basic.h" | |
11 | # include "cgrammar.h" | |
12 | # include "cgrammar_tokens.h" | |
13 | ||
14 | # include "exprChecks.h" | |
15 | # include "aliasChecks.h" | |
16 | # include "exprNodeSList.h" | |
17 | ||
18 | # include "exprData.i" | |
19 | # include "exprDataQuite.i" | |
20 | ||
84c9ffbf | 21 | /*@access exprNode @*/ |
22 | ||
470b7798 | 23 | extern void forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody); |
24 | ||
616915dd | 25 | bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e); |
26 | static bool exprNode_handleError( exprNode p_e); | |
27 | ||
28 | //static cstring exprNode_findConstraints ( exprNode p_e); | |
29 | static bool exprNode_isMultiStatement(exprNode p_e); | |
84c9ffbf | 30 | static void exprNode_multiStatement (exprNode p_e); |
31 | ||
616915dd | 32 | //static void exprNode_constraintPropagateUp (exprNode p_e); |
616915dd | 33 | |
34 | constraintList exprNode_traversTrueEnsuresConstraints (exprNode e); | |
9280addf | 35 | constraintList exprNode_traversFalseEnsuresConstraints (exprNode e); |
616915dd | 36 | |
616915dd | 37 | void mergeResolve (exprNode parent, exprNode child1, exprNode child2); |
38 | exprNode makeDataTypeConstraints (exprNode e); | |
39 | constraintList constraintList_makeFixedArrayConstraints (sRefSet s); | |
40 | constraintList checkCall (exprNode fcn, exprNodeList arglist); | |
41 | ||
9280addf | 42 | void checkArgumentList (exprNode temp, exprNodeList arglist, fileloc sequencePoint); |
43 | ||
616915dd | 44 | //bool exprNode_testd() |
45 | //{ | |
46 | /* if ( ( (exprNode_isError ) ) ) | |
47 | { | |
48 | } | |
49 | if ( ( (e_1 ) ) ) | |
50 | { | |
51 | } | |
52 | */ | |
53 | //} | |
54 | ||
55 | bool exprNode_isUnhandled (exprNode e) | |
56 | { | |
57 | llassert( exprNode_isDefined(e) ); | |
58 | switch (e->kind) | |
59 | { | |
60 | case XPR_INITBLOCK: | |
61 | case XPR_EMPTY: | |
62 | case XPR_LABEL: | |
63 | case XPR_CONST: | |
64 | case XPR_VAR: | |
65 | case XPR_BODY: | |
66 | case XPR_OFFSETOF: | |
67 | case XPR_ALIGNOFT: | |
68 | case XPR_ALIGNOF: | |
69 | case XPR_VAARG: | |
70 | case XPR_ITERCALL: | |
71 | case XPR_ITER: | |
72 | case XPR_CAST: | |
73 | case XPR_GOTO: | |
74 | case XPR_CONTINUE: | |
75 | case XPR_BREAK: | |
76 | case XPR_COMMA: | |
77 | case XPR_COND: | |
78 | case XPR_TOK: | |
79 | case XPR_FTDEFAULT: | |
80 | case XPR_DEFAULT: | |
81 | case XPR_SWITCH: | |
82 | case XPR_FTCASE: | |
83 | case XPR_CASE: | |
84 | // case XPR_INIT: | |
85 | case XPR_NODE: | |
86 | DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) ); | |
87 | return TRUE; | |
88 | /*@notreached@*/ | |
89 | break; | |
90 | default: | |
91 | return FALSE; | |
92 | ||
93 | } | |
94 | /*not reached*/ | |
95 | return FALSE; | |
96 | } | |
97 | ||
98 | bool exprNode_handleError( exprNode e) | |
99 | { | |
100 | if (exprNode_isError (e) || exprNode_isUnhandled(e) ) | |
101 | { | |
102 | static /*@only@*/ cstring error = cstring_undefined; | |
103 | ||
104 | if (!cstring_isDefined (error)) | |
105 | { | |
106 | error = cstring_makeLiteral ("<error>"); | |
107 | } | |
108 | ||
109 | /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/ | |
110 | } | |
111 | return FALSE; | |
112 | } | |
113 | ||
114 | bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) | |
115 | { | |
116 | if (exprNode_isError (e) ) | |
117 | return FALSE; | |
118 | ||
c3e695ff | 119 | e->requiresConstraints = constraintList_makeNew(); |
120 | e->ensuresConstraints = constraintList_makeNew(); | |
121 | e->trueEnsuresConstraints = constraintList_makeNew(); | |
122 | e->falseEnsuresConstraints = constraintList_makeNew(); | |
9280addf | 123 | |
616915dd | 124 | if (exprNode_isUnhandled (e) ) |
125 | { | |
126 | DPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) ); | |
9280addf | 127 | return FALSE; |
616915dd | 128 | } |
129 | ||
130 | ||
131 | // e = makeDataTypeConstraints (e); | |
132 | ||
133 | DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e), | |
134 | fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); | |
135 | ||
136 | if (exprNode_isMultiStatement ( e) ) | |
137 | { | |
138 | exprNode_multiStatement(e); | |
139 | } | |
140 | else | |
141 | { | |
9280addf | 142 | fileloc loc; |
143 | ||
144 | loc = exprNode_getNextSequencePoint(e); | |
145 | exprNode_exprTraverse(e, FALSE, FALSE, loc); | |
146 | ||
616915dd | 147 | // llassert(FALSE); |
148 | return FALSE; | |
149 | } | |
150 | ||
151 | { | |
152 | constraintList c; | |
153 | ||
154 | c = constraintList_makeFixedArrayConstraints (e->uses); | |
155 | e->requiresConstraints = reflectChanges (e->requiresConstraints, c); | |
156 | ||
157 | // e->ensuresConstraints = constraintList_mergeEnsures(c, e->ensuresConstraints); | |
158 | ||
159 | } | |
160 | ||
161 | /* printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) ); | |
162 | printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) ); */ | |
163 | return FALSE; | |
164 | } | |
165 | ||
166 | ||
167 | /* handles multiple statements */ | |
168 | ||
169 | bool exprNode_isMultiStatement(exprNode e) | |
170 | { | |
171 | if (exprNode_handleError (e) != NULL) | |
172 | return FALSE; | |
173 | ||
174 | switch (e->kind) | |
175 | { | |
176 | case XPR_FOR: | |
177 | case XPR_FORPRED: | |
178 | case XPR_IF: | |
179 | case XPR_IFELSE: | |
180 | case XPR_WHILE: | |
181 | case XPR_WHILEPRED: | |
182 | case XPR_DOWHILE: | |
183 | case XPR_BLOCK: | |
184 | case XPR_STMT: | |
185 | case XPR_STMTLIST: | |
186 | return TRUE; | |
187 | default: | |
188 | return FALSE; | |
189 | } | |
190 | ||
191 | } | |
192 | ||
84c9ffbf | 193 | void exprNode_stmt (exprNode e) |
616915dd | 194 | { |
195 | exprNode snode; | |
196 | fileloc loc; | |
9280addf | 197 | char * s; |
198 | ||
616915dd | 199 | if (exprNode_isError(e) ) |
200 | { | |
84c9ffbf | 201 | return; // FALSE; |
616915dd | 202 | } |
c3e695ff | 203 | e->requiresConstraints = constraintList_makeNew(); |
204 | e->ensuresConstraints = constraintList_makeNew(); | |
616915dd | 205 | // e = makeDataTypeConstraints(e); |
206 | ||
207 | ||
208 | DPRINTF(( "STMT:") ); | |
9280addf | 209 | s = exprNode_unparse(e); |
210 | // DPRINTF ( ( message("STMT: %s ") ) ); | |
211 | ||
616915dd | 212 | if (e->kind == XPR_INIT) |
213 | { | |
214 | DPRINTF (("Init") ); | |
215 | DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); | |
216 | loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ | |
84c9ffbf | 217 | exprNode_exprTraverse (e, FALSE, FALSE, loc); |
616915dd | 218 | e->requiresConstraints = exprNode_traversRequiresConstraints(e); |
219 | e->ensuresConstraints = exprNode_traversEnsuresConstraints(e); | |
84c9ffbf | 220 | return; // notError; |
616915dd | 221 | } |
222 | ||
223 | if (e->kind != XPR_STMT) | |
224 | { | |
225 | ||
226 | DPRINTF (("Not Stmt") ); | |
227 | DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); | |
228 | if (exprNode_isMultiStatement (e) ) | |
229 | { | |
230 | return exprNode_multiStatement (e ); | |
231 | } | |
84c9ffbf | 232 | DPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) ); |
233 | return; //TRUE; | |
616915dd | 234 | // llassert(FALSE); |
235 | } | |
236 | ||
237 | DPRINTF (("Stmt") ); | |
238 | DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); | |
239 | ||
240 | snode = exprData_getUopNode (e->edata); | |
241 | ||
242 | /* could be stmt involving multiple statements: | |
243 | i.e. if, while for ect. | |
244 | */ | |
245 | ||
246 | if (exprNode_isMultiStatement (snode)) | |
247 | { | |
84c9ffbf | 248 | exprNode_multiStatement (snode); |
249 | (void) exprNode_copyConstraints (e, snode); | |
250 | return; | |
616915dd | 251 | } |
252 | ||
253 | loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ | |
84c9ffbf | 254 | //notError = |
255 | exprNode_exprTraverse (snode, FALSE, FALSE, loc); | |
616915dd | 256 | e->requiresConstraints = exprNode_traversRequiresConstraints(snode); |
257 | // printf ("For: %s \n", exprNode_unparse (e) ); | |
258 | // printf ("%s\n", constraintList_print(e->requiresConstraints) ); | |
259 | e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode); | |
260 | // printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) ); | |
261 | // llassert(notError); | |
84c9ffbf | 262 | return; // notError; |
616915dd | 263 | |
264 | } | |
265 | ||
266 | ||
84c9ffbf | 267 | void exprNode_stmtList (exprNode e) |
616915dd | 268 | { |
269 | exprNode stmt1, stmt2; | |
270 | if (exprNode_isError (e) ) | |
271 | { | |
84c9ffbf | 272 | return; // FALSE; |
616915dd | 273 | } |
274 | ||
c3e695ff | 275 | e->requiresConstraints = constraintList_makeNew(); |
276 | e->ensuresConstraints = constraintList_makeNew(); | |
616915dd | 277 | // e = makeDataTypeConstraints(e); |
278 | ||
279 | /*Handle case of stmtList with only one statement: | |
280 | The parse tree stores this as stmt instead of stmtList*/ | |
281 | if (e->kind != XPR_STMTLIST) | |
282 | { | |
84c9ffbf | 283 | exprNode_stmt(e); |
284 | return; | |
616915dd | 285 | } |
286 | llassert (e->kind == XPR_STMTLIST); | |
287 | DPRINTF(( "STMTLIST:") ); | |
288 | DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) ); | |
289 | stmt1 = exprData_getPairA (e->edata); | |
290 | stmt2 = exprData_getPairB (e->edata); | |
291 | ||
292 | ||
293 | DPRINTF((" stmtlist ") ); | |
294 | DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) ); | |
295 | ||
296 | exprNode_stmt (stmt1); | |
297 | DPRINTF(("\nstmt after stmtList call " )); | |
298 | ||
299 | exprNode_stmt (stmt2); | |
300 | mergeResolve (e, stmt1, stmt2 ); | |
301 | ||
302 | DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n", | |
303 | constraintList_print(e->requiresConstraints), | |
304 | constraintList_print(e->ensuresConstraints) ) ) ); | |
84c9ffbf | 305 | return; // TRUE; |
a8e557d3 | 306 | } |
307 | ||
616915dd | 308 | exprNode doIf (exprNode e, exprNode test, exprNode body) |
309 | { | |
310 | DPRINTF ((message ("doIf: %s ", exprNode_unparse(e) ) ) ); | |
470b7798 | 311 | |
a8e557d3 | 312 | llassert(exprNode_isDefined(test) ); |
84c9ffbf | 313 | llassert (exprNode_isDefined (e) ); |
314 | llassert (exprNode_isDefined (body) ); | |
616915dd | 315 | |
316 | test->ensuresConstraints = exprNode_traversEnsuresConstraints (test); | |
470b7798 | 317 | test->requiresConstraints = exprNode_traversRequiresConstraints (test); |
318 | ||
616915dd | 319 | test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test); |
320 | ||
c3e695ff | 321 | test->trueEnsuresConstraints = constraintList_substitute(test->trueEnsuresConstraints, test->ensuresConstraints); |
322 | ||
323 | DPRINTF ((message ("doIf: test ensures %s ", constraintList_print(test->ensuresConstraints) ) ) ); | |
324 | ||
325 | DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints) ) ) ); | |
326 | ||
616915dd | 327 | e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints); |
328 | e->requiresConstraints = reflectChanges (e->requiresConstraints, | |
329 | test->ensuresConstraints); | |
470b7798 | 330 | e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints); |
331 | ||
616915dd | 332 | #warning bad |
333 | e->ensuresConstraints = constraintList_copy (test->ensuresConstraints); | |
90bc41f7 | 334 | |
335 | if (exprNode_mayEscape (body) ) | |
336 | { | |
337 | DPRINTF (( message("doIf: the if statement body %s returns or exits", exprNode_unparse(body) ) )); | |
338 | e->ensuresConstraints = constraintList_mergeEnsures (e->ensuresConstraints, | |
470b7798 | 339 | test->falseEnsuresConstraints); |
90bc41f7 | 340 | } |
341 | ||
9280addf | 342 | DPRINTF ((message ("doIf: if requiers %s ", constraintList_print(e->requiresConstraints) ) ) ); |
343 | ||
616915dd | 344 | return e; |
345 | } | |
346 | ||
470b7798 | 347 | /*drl added 3/4/2001 |
348 | Also used for condition i.e. ?: operation | |
349 | ||
350 | Precondition | |
351 | This function assumes that p, trueBranch, falseBranch have have all been traversed | |
352 | for constraints i.e. we assume that exprNode_traversEnsuresConstraints, | |
353 | exprNode_traversRequiresConstraints, exprNode_traversTrueEnsuresConstraints, | |
354 | exprNode_traversFalseEnsuresConstraints have all been run | |
355 | */ | |
356 | ||
357 | ||
358 | exprNode doIfElse (/*@returned@*/ exprNode e, exprNode p, exprNode trueBranch, exprNode falseBranch) | |
359 | { | |
360 | ||
361 | constraintList c1, cons, t, f; | |
362 | ||
363 | // do requires clauses | |
364 | c1 = constraintList_copy (p->ensuresConstraints); | |
365 | ||
366 | t = reflectChanges (trueBranch->requiresConstraints, p->trueEnsuresConstraints); | |
367 | t = reflectChanges (t, p->ensuresConstraints); | |
368 | ||
369 | // e->requiresConstraints = constraintList_copy (cons); | |
370 | ||
371 | cons = reflectChanges (falseBranch->requiresConstraints, p->falseEnsuresConstraints); | |
372 | cons = reflectChanges (cons, c1); | |
373 | ||
374 | e->requiresConstraints = constraintList_mergeRequires (t, cons); | |
375 | e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, p->requiresConstraints); | |
376 | ||
377 | // do ensures clauses | |
378 | // find the the ensures lists for each subbranch | |
379 | t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints); | |
380 | t = constraintList_mergeEnsures (p->ensuresConstraints, t); | |
381 | ||
382 | f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints); | |
383 | f = constraintList_mergeEnsures (p->ensuresConstraints, f); | |
384 | ||
385 | // find ensures for whole if/else statement | |
386 | ||
387 | e->ensuresConstraints = constraintList_logicalOr (t, f); | |
388 | ||
389 | return e; | |
390 | } | |
9280addf | 391 | |
392 | exprNode doWhile (exprNode e, exprNode test, exprNode body) | |
393 | { | |
394 | DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e) ) ) ); | |
395 | return doIf (e, test, body); | |
396 | } | |
397 | ||
616915dd | 398 | constraintList constraintList_makeFixedArrayConstraints (sRefSet s) |
399 | { | |
400 | constraintList ret; | |
470b7798 | 401 | constraint con; |
c3e695ff | 402 | ret = constraintList_makeNew(); |
616915dd | 403 | |
404 | sRefSet_elements (s, el) | |
405 | { | |
406 | // llassert (el); | |
407 | if (sRef_isFixedArray(el) ) | |
408 | { | |
84c9ffbf | 409 | long int size; |
470b7798 | 410 | DPRINTF( (message("%s is a fixed array", |
411 | sRef_unparse(el)) ) ); | |
412 | //if (el->kind == SK_DERIVED) | |
413 | // break; //hack until I find the real problem | |
84c9ffbf | 414 | size = sRef_getArraySize(el); |
616915dd | 415 | DPRINTF( (message("%s is a fixed array with size %d", |
84c9ffbf | 416 | sRef_unparse(el), (int)size) ) ); |
417 | con = constraint_makeSRefSetBufferSize (el, (size - 1)); | |
418 | //con = constraint_makeSRefWriteSafeInt (el, (size - 1)); | |
616915dd | 419 | ret = constraintList_add(ret, con); |
420 | } | |
421 | else | |
422 | { | |
423 | DPRINTF( (message("%s is not a fixed array", | |
424 | sRef_unparse(el)) ) ); | |
470b7798 | 425 | |
426 | ||
427 | if (sRef_isExternallyVisible (el) ) | |
428 | { | |
429 | /*DPRINTF( (message("%s is externally visible", | |
430 | sRef_unparse(el) ) )); | |
431 | con = constraint_makeSRefWriteSafeInt(el, 0); | |
432 | ret = constraintList_add(ret, con); | |
433 | ||
434 | con = constraint_makeSRefReadSafeInt(el, 0); | |
435 | ||
436 | ret = constraintList_add(ret, con);*/ | |
437 | } | |
616915dd | 438 | } |
439 | } | |
440 | end_sRefSet_elements | |
441 | ||
470b7798 | 442 | DPRINTF(( message("constraintList_makeFixedArrayConstraints returning %s", |
443 | constraintList_print(ret) ) )); | |
616915dd | 444 | return ret; |
445 | } | |
446 | ||
447 | exprNode makeDataTypeConstraints (exprNode e) | |
448 | { | |
449 | constraintList c; | |
450 | DPRINTF(("makeDataTypeConstraints")); | |
451 | ||
452 | c = constraintList_makeFixedArrayConstraints (e->uses); | |
453 | ||
454 | e->ensuresConstraints = constraintList_addList (e->ensuresConstraints, c); | |
455 | ||
456 | return e; | |
457 | } | |
458 | ||
459 | void doFor (exprNode e, exprNode forPred, exprNode forBody) | |
460 | { | |
461 | exprNode init, test, inc; | |
462 | //merge the constraints: modle as if statement | |
463 | /* init | |
464 | if (test) | |
465 | for body | |
466 | inc */ | |
467 | init = exprData_getTripleInit (forPred->edata); | |
468 | test = exprData_getTripleTest (forPred->edata); | |
469 | inc = exprData_getTripleInc (forPred->edata); | |
470 | ||
471 | if ( ( (exprNode_isError (test) /*|| (exprNode_isError(init) )*/ ) || (exprNode_isError (inc) ) ) ) | |
472 | { | |
473 | DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e) ) ) ); | |
474 | return; | |
475 | } | |
476 | ||
477 | forLoopHeuristics(e, forPred, forBody); | |
478 | ||
479 | e->requiresConstraints = reflectChanges (forBody->requiresConstraints, test->ensuresConstraints); | |
480 | e->requiresConstraints = reflectChanges (e->requiresConstraints, test->trueEnsuresConstraints); | |
481 | e->requiresConstraints = reflectChanges (e->requiresConstraints, forPred->ensuresConstraints); | |
482 | ||
483 | if (!forBody->canBreak) | |
484 | { | |
485 | e->ensuresConstraints = constraintList_addList(e->ensuresConstraints, forPred->ensuresConstraints); | |
486 | e->ensuresConstraints = constraintList_addList(e->ensuresConstraints, test->falseEnsuresConstraints); | |
84c9ffbf | 487 | forPred->ensuresConstraints = constraintList_undefined; |
488 | test->falseEnsuresConstraints = constraintList_undefined; | |
616915dd | 489 | } |
490 | else | |
491 | { | |
492 | DPRINTF(("Can break") ); | |
493 | } | |
494 | ||
495 | } | |
496 | ||
470b7798 | 497 | exprNode doSwitch (/*@returned@*/ exprNode e) |
498 | { | |
499 | exprNode body; | |
500 | exprData data; | |
501 | ||
502 | data = e->edata; | |
503 | llassert(FALSE); | |
90bc41f7 | 504 | //DPRINTF (( message ("doSwitch for: switch (%s) %s", |
470b7798 | 505 | // exprNode_unparse (exprData_getPairA (data)), |
506 | // exprNode_unparse (exprData_getPairB (data))) )); | |
507 | ||
508 | body = exprData_getPairB (data); | |
509 | ||
510 | // exprNode_generateConstraints(body); | |
511 | ||
512 | // e->requiresConstraints = constraintList_copy ( body->requiresConstraints ); | |
513 | //e->ensuresConstraints = constraintList_copy ( body->ensuresConstraints ); | |
514 | ||
515 | return e; | |
516 | } | |
9280addf | 517 | |
518 | ||
84c9ffbf | 519 | void exprNode_multiStatement (exprNode e) |
616915dd | 520 | { |
521 | ||
522 | bool ret; | |
523 | exprData data; | |
524 | exprNode e1, e2; | |
525 | exprNode p, trueBranch, falseBranch; | |
526 | exprNode forPred, forBody; | |
470b7798 | 527 | exprNode test; |
528 | // constraintList t, f; | |
c3e695ff | 529 | e->requiresConstraints = constraintList_makeNew(); |
530 | e->ensuresConstraints = constraintList_makeNew(); | |
531 | e->trueEnsuresConstraints = constraintList_makeNew(); | |
532 | e->falseEnsuresConstraints = constraintList_makeNew(); | |
616915dd | 533 | |
534 | // e = makeDataTypeConstraints(e); | |
535 | ||
536 | DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e), | |
537 | fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); | |
538 | ||
539 | if (exprNode_handleError (e)) | |
540 | { | |
84c9ffbf | 541 | return; // FALSE; |
616915dd | 542 | } |
543 | ||
544 | data = e->edata; | |
545 | ||
546 | ret = TRUE; | |
547 | ||
548 | switch (e->kind) | |
549 | { | |
550 | ||
551 | case XPR_FOR: | |
552 | // ret = message ("%s %s", | |
553 | forPred = exprData_getPairA (data); | |
554 | forBody = exprData_getPairB (data); | |
555 | ||
556 | //first generate the constraints | |
557 | exprNode_generateConstraints (forPred); | |
558 | exprNode_generateConstraints (forBody); | |
559 | ||
560 | ||
561 | doFor (e, forPred, forBody); | |
562 | ||
563 | break; | |
564 | ||
565 | case XPR_FORPRED: | |
566 | // ret = message ("for (%s; %s; %s)", | |
567 | exprNode_generateConstraints (exprData_getTripleInit (data) ); | |
568 | test = exprData_getTripleTest (data); | |
569 | exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e)); | |
9280addf | 570 | exprNode_generateConstraints (exprData_getTripleInc (data) ); |
571 | ||
616915dd | 572 | if (!exprNode_isError(test) ) |
573 | test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test); | |
574 | ||
575 | exprNode_generateConstraints (exprData_getTripleInc (data)); | |
576 | break; | |
9280addf | 577 | |
578 | case XPR_WHILE: | |
579 | e1 = exprData_getPairA (data); | |
580 | e2 = exprData_getPairB (data); | |
581 | ||
582 | exprNode_exprTraverse (e1, | |
583 | FALSE, FALSE, exprNode_loc(e1)); | |
584 | ||
585 | exprNode_generateConstraints (e2); | |
586 | ||
587 | e = doWhile (e, e1, e2); | |
588 | ||
589 | break; | |
590 | ||
616915dd | 591 | case XPR_IF: |
592 | DPRINTF(( "IF:") ); | |
593 | DPRINTF ((exprNode_unparse(e) ) ); | |
594 | // ret = message ("if (%s) %s", | |
595 | e1 = exprData_getPairA (data); | |
596 | e2 = exprData_getPairB (data); | |
597 | ||
598 | exprNode_exprTraverse (e1, | |
599 | FALSE, FALSE, exprNode_loc(e1)); | |
600 | ||
601 | exprNode_generateConstraints (e2); | |
602 | ||
603 | e = doIf (e, e1, e2); | |
604 | ||
605 | ||
606 | // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data)); | |
607 | break; | |
9280addf | 608 | |
609 | ||
616915dd | 610 | case XPR_IFELSE: |
611 | DPRINTF(("Starting IFELSE")); | |
612 | // ret = message ("if (%s) %s else %s", | |
613 | p = exprData_getTriplePred (data); | |
614 | trueBranch = exprData_getTripleTrue (data); | |
615 | falseBranch = exprData_getTripleFalse (data); | |
616 | ||
617 | exprNode_exprTraverse (p, | |
618 | FALSE, FALSE, exprNode_loc(p)); | |
619 | exprNode_generateConstraints (trueBranch); | |
620 | exprNode_generateConstraints (falseBranch); | |
621 | ||
9280addf | 622 | p->ensuresConstraints = exprNode_traversEnsuresConstraints (p); |
470b7798 | 623 | p->requiresConstraints = exprNode_traversRequiresConstraints (p); |
624 | ||
9280addf | 625 | p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p); |
470b7798 | 626 | p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p); |
616915dd | 627 | |
470b7798 | 628 | e = doIfElse (e, p, trueBranch, falseBranch); |
616915dd | 629 | DPRINTF( ("Done IFELSE") ); |
630 | break; | |
9280addf | 631 | |
616915dd | 632 | case XPR_DOWHILE: |
470b7798 | 633 | |
634 | e2 = (exprData_getPairB (data)); | |
635 | e1 = (exprData_getPairA (data)); | |
636 | ||
637 | DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1) ) )); | |
638 | exprNode_generateConstraints (e2); | |
639 | exprNode_generateConstraints (e1); | |
640 | e = exprNode_copyConstraints (e, e2); | |
641 | DPRINTF ((message ("e = %s ", constraintList_print(e->requiresConstraints) ) )); | |
642 | ||
616915dd | 643 | break; |
644 | ||
645 | case XPR_BLOCK: | |
646 | // ret = message ("{ %s }", | |
647 | exprNode_generateConstraints (exprData_getSingle (data)); | |
648 | e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints ); | |
649 | e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints ); | |
650 | // e->constraints = (exprData_getSingle (data))->constraints; | |
651 | break; | |
652 | ||
470b7798 | 653 | case XPR_SWITCH: |
654 | e = doSwitch (e); | |
655 | break; | |
616915dd | 656 | case XPR_STMT: |
657 | case XPR_STMTLIST: | |
84c9ffbf | 658 | exprNode_stmtList (e); |
659 | return ; | |
616915dd | 660 | /*@notreached@*/ |
661 | break; | |
662 | default: | |
663 | ret=FALSE; | |
664 | } | |
84c9ffbf | 665 | return; // ret; |
616915dd | 666 | } |
667 | ||
668 | bool lltok_isBoolean_Op (lltok tok) | |
669 | { | |
670 | /*this should really be a switch statement but | |
671 | I don't want to violate the abstraction | |
672 | maybe this should go in lltok.c */ | |
673 | ||
674 | if (lltok_isEq_Op (tok) ) | |
675 | { | |
676 | return TRUE; | |
677 | } | |
678 | if (lltok_isAnd_Op (tok) ) | |
679 | ||
680 | { | |
681 | ||
682 | return TRUE; | |
683 | } | |
684 | if (lltok_isOr_Op (tok) ) | |
685 | { | |
686 | return TRUE; | |
687 | } | |
688 | ||
689 | if (lltok_isGt_Op (tok) ) | |
690 | { | |
691 | return TRUE; | |
692 | } | |
693 | if (lltok_isLt_Op (tok) ) | |
694 | { | |
695 | return TRUE; | |
696 | } | |
697 | ||
698 | if (lltok_isLe_Op (tok) ) | |
699 | { | |
700 | return TRUE; | |
701 | } | |
702 | ||
703 | if (lltok_isGe_Op (tok) ) | |
704 | { | |
705 | return TRUE; | |
706 | } | |
707 | ||
708 | return FALSE; | |
709 | ||
710 | } | |
711 | ||
712 | ||
84c9ffbf | 713 | void exprNode_booleanTraverse (exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv, fileloc sequencePoint) |
616915dd | 714 | { |
715 | constraint cons; | |
716 | exprNode t1, t2; | |
717 | exprData data; | |
718 | lltok tok; | |
719 | constraintList tempList; | |
720 | data = e->edata; | |
721 | ||
722 | tok = exprData_getOpTok (data); | |
723 | ||
724 | ||
725 | t1 = exprData_getOpA (data); | |
726 | t2 = exprData_getOpB (data); | |
727 | ||
728 | ||
729 | /* arithmetic tests */ | |
730 | ||
731 | if (lltok_isEq_Op (tok) ) | |
732 | { | |
733 | cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); | |
734 | e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); | |
735 | } | |
736 | ||
737 | ||
738 | if (lltok_isLt_Op (tok) ) | |
739 | { | |
740 | cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint); | |
741 | e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); | |
742 | cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint); | |
743 | e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); | |
744 | } | |
745 | ||
746 | ||
747 | if (lltok_isGe_Op (tok) ) | |
748 | { | |
749 | ||
750 | cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint); | |
751 | e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); | |
752 | ||
753 | cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint); | |
754 | e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); | |
755 | ||
756 | } | |
757 | ||
758 | ||
759 | if (lltok_isGt_Op (tok) ) | |
760 | { | |
761 | cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint); | |
762 | e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); | |
763 | cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint); | |
764 | e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); | |
765 | } | |
766 | ||
767 | if (lltok_isLe_Op (tok) ) | |
768 | { | |
769 | cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint); | |
770 | e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); | |
771 | ||
772 | cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint); | |
773 | e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); | |
774 | } | |
775 | ||
776 | ||
777 | ||
778 | /*Logical operations */ | |
779 | ||
780 | if (lltok_isAnd_Op (tok) ) | |
781 | ||
782 | { | |
783 | //true ensures | |
784 | tempList = constraintList_copy (t1->trueEnsuresConstraints); | |
785 | tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints); | |
786 | e->trueEnsuresConstraints = constraintList_addList(e->trueEnsuresConstraints, tempList); | |
787 | ||
788 | //false ensures: fens t1 or tens t1 and fens t2 | |
789 | tempList = constraintList_copy (t1->trueEnsuresConstraints); | |
790 | tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints); | |
791 | tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints); | |
792 | e->falseEnsuresConstraints =constraintList_addList(e->falseEnsuresConstraints, tempList); | |
793 | ||
794 | } | |
84c9ffbf | 795 | else if (lltok_isOr_Op (tok) ) |
796 | { | |
616915dd | 797 | //false ensures |
798 | tempList = constraintList_copy (t1->falseEnsuresConstraints); | |
799 | tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints); | |
800 | e->falseEnsuresConstraints = constraintList_addList(e->falseEnsuresConstraints, tempList); | |
801 | ||
802 | //true ensures: tens t1 or fens t1 and tens t2 | |
803 | tempList = constraintList_copy (t1->falseEnsuresConstraints); | |
804 | tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints); | |
805 | tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints); | |
806 | e->trueEnsuresConstraints =constraintList_addList(e->trueEnsuresConstraints, tempList); | |
807 | ||
808 | } | |
84c9ffbf | 809 | else |
810 | { | |
811 | DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok) ) )); | |
812 | } | |
616915dd | 813 | |
814 | } | |
815 | ||
84c9ffbf | 816 | void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint) |
616915dd | 817 | { |
9280addf | 818 | exprNode t1, t2, fcn; |
616915dd | 819 | lltok tok; |
820 | bool handledExprNode; | |
821 | exprData data; | |
822 | constraint cons; | |
823 | ||
470b7798 | 824 | if (exprNode_isError(e) ) |
825 | { | |
84c9ffbf | 826 | return; // FALSE; |
470b7798 | 827 | } |
828 | ||
829 | DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e), | |
616915dd | 830 | fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); |
470b7798 | 831 | |
c3e695ff | 832 | e->requiresConstraints = constraintList_makeNew(); |
833 | e->ensuresConstraints = constraintList_makeNew(); | |
834 | e->trueEnsuresConstraints = constraintList_makeNew();; | |
835 | e->falseEnsuresConstraints = constraintList_makeNew();; | |
470b7798 | 836 | |
837 | if (exprNode_isUnhandled (e) ) | |
616915dd | 838 | { |
84c9ffbf | 839 | return; // FALSE; |
616915dd | 840 | } |
841 | // e = makeDataTypeConstraints (e); | |
842 | ||
843 | handledExprNode = TRUE; | |
844 | ||
845 | data = e->edata; | |
846 | ||
847 | switch (e->kind) | |
848 | { | |
849 | ||
850 | ||
851 | case XPR_WHILEPRED: | |
852 | t1 = exprData_getSingle (data); | |
853 | exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint); | |
854 | e = exprNode_copyConstraints (e, t1); | |
855 | break; | |
856 | ||
857 | case XPR_FETCH: | |
858 | ||
859 | if (definatelv ) | |
860 | { | |
861 | t1 = (exprData_getPairA (data) ); | |
862 | t2 = (exprData_getPairB (data) ); | |
863 | cons = constraint_makeWriteSafeExprNode (t1, t2); | |
864 | } | |
865 | else | |
866 | { | |
867 | t1 = (exprData_getPairA (data) ); | |
868 | t2 = (exprData_getPairB (data) ); | |
869 | cons = constraint_makeReadSafeExprNode (t1, t2 ); | |
870 | } | |
871 | ||
872 | e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); | |
873 | cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint); | |
874 | e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); | |
875 | ||
9280addf | 876 | cons = constraint_makeEnsureLteMaxRead (t2, t1); |
616915dd | 877 | e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); |
878 | ||
879 | // cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint); | |
880 | // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); | |
881 | ||
882 | exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint); | |
883 | exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint); | |
884 | ||
885 | /*@i325 Should check which is array/index. */ | |
886 | break; | |
887 | ||
888 | case XPR_PARENS: | |
889 | exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint); | |
890 | // e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined); | |
891 | break; | |
892 | case XPR_INIT: | |
893 | /* //t1 = exprData_getInitId (data); */ | |
894 | t2 = exprData_getInitNode (data); | |
895 | //exprNode_exprTraverse (t1, TRUE, FALSE, sequencePoint ); | |
896 | ||
897 | exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint ); | |
898 | ||
899 | /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */ | |
900 | if ( (!exprNode_isError (e)) && (!exprNode_isError(t2)) ) | |
901 | { | |
902 | cons = constraint_makeEnsureEqual (e, t2, sequencePoint); | |
903 | e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); | |
904 | } | |
905 | ||
906 | break; | |
907 | case XPR_ASSIGN: | |
908 | t1 = exprData_getOpA (data); | |
909 | t2 = exprData_getOpB (data); | |
910 | exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint ); | |
84c9ffbf | 911 | //lltok_unparse (exprData_getOpTok (data)); |
912 | #warning check this for += -= etc | |
616915dd | 913 | exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint ); |
914 | ||
915 | /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */ | |
916 | if ( (!exprNode_isError (t1)) && (!exprNode_isError(t2)) ) | |
917 | { | |
918 | cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); | |
919 | e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); | |
920 | } | |
921 | break; | |
922 | case XPR_OP: | |
923 | t1 = exprData_getOpA (data); | |
924 | t2 = exprData_getOpB (data); | |
925 | ||
926 | exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint ); | |
927 | tok = exprData_getOpTok (data); | |
928 | exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint ); | |
929 | ||
930 | if (lltok_isBoolean_Op (tok) ) | |
931 | exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint); | |
932 | ||
933 | // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data)); | |
934 | break; | |
935 | case XPR_SIZEOFT: | |
84c9ffbf | 936 | #warning make sure the case can be ignored.. |
616915dd | 937 | |
938 | break; | |
939 | ||
940 | case XPR_SIZEOF: | |
941 | exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint ); | |
942 | // e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined); | |
943 | break; | |
944 | ||
945 | case XPR_CALL: | |
9280addf | 946 | fcn = exprData_getFcn(data); |
947 | ||
948 | exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint ); | |
9280addf | 949 | DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data) ) ) ) ); |
616915dd | 950 | |
9280addf | 951 | fcn->requiresConstraints = constraintList_addList (fcn->requiresConstraints, |
952 | checkCall (fcn, exprData_getArgs (data) ) ); | |
616915dd | 953 | |
9280addf | 954 | fcn->ensuresConstraints = constraintList_addList (fcn->ensuresConstraints, |
955 | getPostConditions(fcn, exprData_getArgs (data),e ) ); | |
956 | ||
957 | t1 = exprNode_createNew (exprNode_getType (e) ); | |
958 | ||
959 | checkArgumentList (t1, exprData_getArgs(data), sequencePoint); | |
616915dd | 960 | |
9280addf | 961 | |
962 | mergeResolve (e, t1, fcn); | |
963 | ||
616915dd | 964 | // e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) ); |
965 | break; | |
966 | ||
967 | case XPR_RETURN: | |
968 | exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint ); | |
969 | break; | |
970 | ||
971 | case XPR_NULLRETURN: | |
84c9ffbf | 972 | |
616915dd | 973 | break; |
974 | ||
975 | ||
976 | case XPR_FACCESS: | |
977 | exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint ); | |
616915dd | 978 | break; |
979 | ||
980 | case XPR_ARROW: | |
981 | exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint ); | |
616915dd | 982 | break; |
983 | ||
984 | case XPR_STRINGLITERAL: | |
84c9ffbf | 985 | |
616915dd | 986 | break; |
987 | ||
988 | case XPR_NUMLIT: | |
84c9ffbf | 989 | |
616915dd | 990 | break; |
991 | ||
992 | case XPR_PREOP: | |
993 | t1 = exprData_getUopNode(data); | |
994 | tok = (exprData_getUopTok (data)); | |
995 | //lltok_unparse (exprData_getUopTok (data)); | |
996 | exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint ); | |
997 | /*handle * pointer access */ | |
998 | if (lltok_isInc_Op (tok) ) | |
999 | { | |
1000 | DPRINTF(("doing ++(var)")); | |
1001 | t1 = exprData_getUopNode (data); | |
1002 | cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint ); | |
1003 | e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); | |
1004 | } | |
1005 | else if (lltok_isDec_Op (tok) ) | |
1006 | { | |
1007 | DPRINTF(("doing --(var)")); | |
1008 | t1 = exprData_getUopNode (data); | |
1009 | cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint ); | |
1010 | e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); | |
1011 | } | |
84c9ffbf | 1012 | else if (lltok_isMult( tok ) ) |
616915dd | 1013 | { |
1014 | if (definatelv) | |
1015 | { | |
1016 | cons = constraint_makeWriteSafeInt (t1, 0); | |
1017 | } | |
1018 | else | |
1019 | { | |
1020 | cons = constraint_makeReadSafeInt (t1, 0); | |
1021 | } | |
1022 | e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); | |
1023 | } | |
84c9ffbf | 1024 | else if (lltok_isNot_Op (tok) ) |
1025 | /* ! expr */ | |
616915dd | 1026 | { |
1027 | e->trueEnsuresConstraints = constraintList_copy (t1->falseEnsuresConstraints); | |
1028 | e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints); | |
1029 | } | |
84c9ffbf | 1030 | else if (lltok_isAmpersand_Op (tok) ) |
1031 | { | |
1032 | break; | |
1033 | } | |
1034 | else | |
1035 | { | |
1036 | llcontbug((message("Unsupported preop in %s", exprNode_unparse(e) ) )); | |
1037 | BADEXIT; | |
1038 | } | |
616915dd | 1039 | break; |
1040 | ||
1041 | case XPR_POSTOP: | |
1042 | ||
1043 | exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint ); | |
84c9ffbf | 1044 | |
616915dd | 1045 | if (lltok_isInc_Op (exprData_getUopTok (data) ) ) |
1046 | { | |
1047 | DPRINTF(("doing ++")); | |
1048 | t1 = exprData_getUopNode (data); | |
1049 | cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint ); | |
1050 | e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); | |
1051 | } | |
1052 | if (lltok_isDec_Op (exprData_getUopTok (data) ) ) | |
1053 | { | |
1054 | DPRINTF(("doing --")); | |
1055 | t1 = exprData_getUopNode (data); | |
1056 | cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint ); | |
1057 | e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); | |
1058 | } | |
1059 | break; | |
470b7798 | 1060 | case XPR_CAST: |
1061 | llassert(FALSE); | |
1062 | exprNode_exprTraverse (exprData_getCastNode (data), definatelv, definaterv, sequencePoint ); | |
1063 | break; | |
1064 | case XPR_COND: | |
1065 | { | |
1066 | exprNode pred, true, false; | |
1067 | llassert(FALSE); | |
1068 | pred = exprData_getTriplePred (data); | |
1069 | true = exprData_getTripleTrue (data); | |
1070 | false = exprData_getTripleFalse (data); | |
1071 | ||
1072 | exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint ); | |
1073 | pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred); | |
1074 | pred->requiresConstraints = exprNode_traversRequiresConstraints(pred); | |
1075 | ||
1076 | pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred); | |
1077 | pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred); | |
1078 | ||
1079 | exprNode_exprTraverse (true, FALSE, TRUE, sequencePoint ); | |
1080 | true->ensuresConstraints = exprNode_traversEnsuresConstraints(true); | |
1081 | true->requiresConstraints = exprNode_traversRequiresConstraints(true); | |
1082 | ||
1083 | true->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(true); | |
1084 | true->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(true); | |
1085 | ||
1086 | exprNode_exprTraverse (false, FALSE, TRUE, sequencePoint ); | |
1087 | false->ensuresConstraints = exprNode_traversEnsuresConstraints(false); | |
1088 | false->requiresConstraints = exprNode_traversRequiresConstraints(false); | |
1089 | ||
1090 | false->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(false); | |
1091 | false->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(false); | |
1092 | ||
1093 | ||
1094 | /* if pred is true e equals true otherwise pred equals false */ | |
1095 | ||
1096 | cons = constraint_makeEnsureEqual (e, true, sequencePoint); | |
1097 | true->ensuresConstraints = constraintList_add(true->ensuresConstraints, cons); | |
1098 | ||
1099 | cons = constraint_makeEnsureEqual (e, true, sequencePoint); | |
1100 | false->ensuresConstraints = constraintList_add(false->ensuresConstraints, cons); | |
1101 | ||
1102 | e = doIfElse (e, pred, true, false); | |
1103 | ||
1104 | } | |
1105 | break; | |
1106 | case XPR_COMMA: | |
1107 | llassert(FALSE); | |
1108 | t1 = exprData_getPairA (data); | |
1109 | t2 = exprData_getPairB (data); | |
1110 | /* we essiantially treat this like expr1; expr2 | |
1111 | of course sequencePoint isn't adjusted so this isn't completely accurate | |
1112 | problems../ */ | |
1113 | exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint ); | |
1114 | exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint ); | |
1115 | mergeResolve (e, t1, t2); | |
1116 | break; | |
1117 | ||
616915dd | 1118 | default: |
1119 | handledExprNode = FALSE; | |
1120 | } | |
1121 | ||
1122 | e->requiresConstraints = constraintList_preserveOrig ( e->requiresConstraints); | |
1123 | e->ensuresConstraints = constraintList_preserveOrig ( e->ensuresConstraints); | |
9280addf | 1124 | e->requiresConstraints = constraintList_addGeneratingExpr ( e->requiresConstraints, e); |
1125 | ||
1126 | e->ensuresConstraints = constraintList_addGeneratingExpr ( e->ensuresConstraints, e); | |
1127 | ||
1128 | DPRINTF((message ("ensures constraint for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) )); | |
616915dd | 1129 | |
84c9ffbf | 1130 | return; // handledExprNode; |
616915dd | 1131 | } |
1132 | ||
1133 | ||
1134 | constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) | |
1135 | { | |
470b7798 | 1136 | exprNode t1; |
616915dd | 1137 | |
1138 | bool handledExprNode; | |
1139 | // char * mes; | |
1140 | exprData data; | |
1141 | constraintList ret; | |
1142 | ||
1143 | if (exprNode_handleError (e)) | |
1144 | { | |
c3e695ff | 1145 | ret = constraintList_makeNew(); |
616915dd | 1146 | return ret; |
1147 | } | |
1148 | ret = constraintList_copy (e->trueEnsuresConstraints ); | |
1149 | ||
1150 | handledExprNode = TRUE; | |
1151 | ||
1152 | data = e->edata; | |
1153 | ||
1154 | switch (e->kind) | |
1155 | { | |
9280addf | 1156 | case XPR_WHILEPRED: |
1157 | t1 = exprData_getSingle (data); | |
1158 | ret = constraintList_addList ( ret,exprNode_traversTrueEnsuresConstraints (t1) ); | |
1159 | break; | |
616915dd | 1160 | |
1161 | case XPR_FETCH: | |
1162 | ||
1163 | ret = constraintList_addList (ret, | |
1164 | exprNode_traversTrueEnsuresConstraints | |
1165 | (exprData_getPairA (data) ) ); | |
1166 | ||
1167 | ret = constraintList_addList (ret, | |
1168 | exprNode_traversTrueEnsuresConstraints | |
1169 | (exprData_getPairB (data) ) ); | |
1170 | break; | |
1171 | case XPR_PREOP: | |
1172 | ||
1173 | ret = constraintList_addList (ret, | |
1174 | exprNode_traversTrueEnsuresConstraints | |
1175 | (exprData_getUopNode (data) ) ); | |
1176 | break; | |
1177 | ||
1178 | case XPR_PARENS: | |
1179 | ret = constraintList_addList (ret, exprNode_traversTrueEnsuresConstraints | |
1180 | (exprData_getUopNode (data) ) ); | |
1181 | break; | |
1182 | case XPR_ASSIGN: | |
1183 | ret = constraintList_addList (ret, | |
1184 | exprNode_traversTrueEnsuresConstraints | |
1185 | (exprData_getOpA (data) ) ); | |
1186 | ||
1187 | ret = constraintList_addList (ret, | |
1188 | exprNode_traversTrueEnsuresConstraints | |
1189 | (exprData_getOpB (data) ) ); | |
1190 | break; | |
1191 | case XPR_OP: | |
1192 | ret = constraintList_addList (ret, | |
1193 | exprNode_traversTrueEnsuresConstraints | |
1194 | (exprData_getOpA (data) ) ); | |
1195 | ||
1196 | ret = constraintList_addList (ret, | |
1197 | exprNode_traversTrueEnsuresConstraints | |
1198 | (exprData_getOpB (data) ) ); | |
1199 | break; | |
1200 | case XPR_SIZEOFT: | |
1201 | ||
1202 | // ctype_unparse (qtype_getType (exprData_getType (data) ) ); | |
1203 | ||
1204 | break; | |
1205 | ||
1206 | case XPR_SIZEOF: | |
1207 | ||
1208 | ret = constraintList_addList (ret, | |
1209 | exprNode_traversTrueEnsuresConstraints | |
1210 | (exprData_getSingle (data) ) ); | |
1211 | break; | |
1212 | ||
1213 | case XPR_CALL: | |
1214 | ret = constraintList_addList (ret, | |
1215 | exprNode_traversTrueEnsuresConstraints | |
1216 | (exprData_getFcn (data) ) ); | |
1217 | /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); | |
1218 | break; | |
1219 | ||
1220 | case XPR_RETURN: | |
1221 | ret = constraintList_addList (ret, | |
1222 | exprNode_traversTrueEnsuresConstraints | |
1223 | (exprData_getSingle (data) ) ); | |
1224 | break; | |
1225 | ||
1226 | case XPR_NULLRETURN: | |
1227 | // cstring_makeLiteral ("return");; | |
1228 | break; | |
1229 | ||
1230 | case XPR_FACCESS: | |
1231 | ret = constraintList_addList (ret, | |
1232 | exprNode_traversTrueEnsuresConstraints | |
1233 | (exprData_getFieldNode (data) ) ); | |
1234 | //exprData_getFieldName (data) ; | |
1235 | break; | |
1236 | ||
1237 | case XPR_ARROW: | |
1238 | ret = constraintList_addList (ret, | |
1239 | exprNode_traversTrueEnsuresConstraints | |
1240 | (exprData_getFieldNode (data) ) ); | |
1241 | // exprData_getFieldName (data); | |
1242 | break; | |
1243 | ||
1244 | case XPR_STRINGLITERAL: | |
1245 | // cstring_copy (exprData_getLiteral (data)); | |
1246 | break; | |
1247 | ||
1248 | case XPR_NUMLIT: | |
1249 | // cstring_copy (exprData_getLiteral (data)); | |
1250 | break; | |
1251 | case XPR_POSTOP: | |
1252 | ||
1253 | ret = constraintList_addList (ret, | |
1254 | exprNode_traversTrueEnsuresConstraints | |
1255 | (exprData_getUopNode (data) ) ); | |
1256 | break; | |
470b7798 | 1257 | |
1258 | case XPR_CAST: | |
1259 | ||
1260 | ret = constraintList_addList (ret, | |
1261 | exprNode_traversTrueEnsuresConstraints | |
1262 | (exprData_getCastNode (data) ) ); | |
470b7798 | 1263 | break; |
84c9ffbf | 1264 | |
616915dd | 1265 | default: |
1266 | break; | |
1267 | } | |
1268 | ||
1269 | return ret; | |
1270 | } | |
1271 | ||
9280addf | 1272 | constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) |
1273 | { | |
470b7798 | 1274 | exprNode t1; |
9280addf | 1275 | |
1276 | bool handledExprNode; | |
1277 | // char * mes; | |
1278 | exprData data; | |
1279 | constraintList ret; | |
1280 | ||
1281 | if (exprNode_handleError (e)) | |
1282 | { | |
c3e695ff | 1283 | ret = constraintList_makeNew(); |
9280addf | 1284 | return ret; |
1285 | } | |
1286 | ret = constraintList_copy (e->falseEnsuresConstraints ); | |
1287 | ||
1288 | handledExprNode = TRUE; | |
1289 | ||
1290 | data = e->edata; | |
1291 | ||
1292 | switch (e->kind) | |
1293 | { | |
1294 | case XPR_WHILEPRED: | |
1295 | t1 = exprData_getSingle (data); | |
1296 | ret = constraintList_addList ( ret,exprNode_traversFalseEnsuresConstraints (t1) ); | |
1297 | break; | |
1298 | ||
1299 | case XPR_FETCH: | |
1300 | ||
1301 | ret = constraintList_addList (ret, | |
1302 | exprNode_traversFalseEnsuresConstraints | |
1303 | (exprData_getPairA (data) ) ); | |
1304 | ||
1305 | ret = constraintList_addList (ret, | |
1306 | exprNode_traversFalseEnsuresConstraints | |
1307 | (exprData_getPairB (data) ) ); | |
1308 | break; | |
1309 | case XPR_PREOP: | |
1310 | ||
1311 | ret = constraintList_addList (ret, | |
1312 | exprNode_traversFalseEnsuresConstraints | |
1313 | (exprData_getUopNode (data) ) ); | |
1314 | break; | |
1315 | ||
1316 | case XPR_PARENS: | |
1317 | ret = constraintList_addList (ret, exprNode_traversFalseEnsuresConstraints | |
1318 | (exprData_getUopNode (data) ) ); | |
1319 | break; | |
1320 | case XPR_ASSIGN: | |
1321 | ret = constraintList_addList (ret, | |
1322 | exprNode_traversFalseEnsuresConstraints | |
1323 | (exprData_getOpA (data) ) ); | |
1324 | ||
1325 | ret = constraintList_addList (ret, | |
1326 | exprNode_traversFalseEnsuresConstraints | |
1327 | (exprData_getOpB (data) ) ); | |
1328 | break; | |
1329 | case XPR_OP: | |
1330 | ret = constraintList_addList (ret, | |
1331 | exprNode_traversFalseEnsuresConstraints | |
1332 | (exprData_getOpA (data) ) ); | |
1333 | ||
1334 | ret = constraintList_addList (ret, | |
1335 | exprNode_traversFalseEnsuresConstraints | |
1336 | (exprData_getOpB (data) ) ); | |
1337 | break; | |
1338 | case XPR_SIZEOFT: | |
1339 | ||
1340 | // ctype_unparse (qtype_getType (exprData_getType (data) ) ); | |
1341 | ||
1342 | break; | |
1343 | ||
1344 | case XPR_SIZEOF: | |
1345 | ||
1346 | ret = constraintList_addList (ret, | |
1347 | exprNode_traversFalseEnsuresConstraints | |
1348 | (exprData_getSingle (data) ) ); | |
1349 | break; | |
1350 | ||
1351 | case XPR_CALL: | |
1352 | ret = constraintList_addList (ret, | |
1353 | exprNode_traversFalseEnsuresConstraints | |
1354 | (exprData_getFcn (data) ) ); | |
1355 | /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); | |
1356 | break; | |
1357 | ||
1358 | case XPR_RETURN: | |
1359 | ret = constraintList_addList (ret, | |
1360 | exprNode_traversFalseEnsuresConstraints | |
1361 | (exprData_getSingle (data) ) ); | |
1362 | break; | |
1363 | ||
1364 | case XPR_NULLRETURN: | |
1365 | // cstring_makeLiteral ("return");; | |
1366 | break; | |
1367 | ||
1368 | case XPR_FACCESS: | |
1369 | ret = constraintList_addList (ret, | |
1370 | exprNode_traversFalseEnsuresConstraints | |
1371 | (exprData_getFieldNode (data) ) ); | |
1372 | //exprData_getFieldName (data) ; | |
1373 | break; | |
1374 | ||
1375 | case XPR_ARROW: | |
1376 | ret = constraintList_addList (ret, | |
1377 | exprNode_traversFalseEnsuresConstraints | |
1378 | (exprData_getFieldNode (data) ) ); | |
1379 | // exprData_getFieldName (data); | |
1380 | break; | |
1381 | ||
1382 | case XPR_STRINGLITERAL: | |
1383 | // cstring_copy (exprData_getLiteral (data)); | |
1384 | break; | |
1385 | ||
1386 | case XPR_NUMLIT: | |
1387 | // cstring_copy (exprData_getLiteral (data)); | |
1388 | break; | |
1389 | case XPR_POSTOP: | |
1390 | ||
1391 | ret = constraintList_addList (ret, | |
1392 | exprNode_traversFalseEnsuresConstraints | |
1393 | (exprData_getUopNode (data) ) ); | |
1394 | break; | |
470b7798 | 1395 | |
1396 | case XPR_CAST: | |
1397 | ||
1398 | ret = constraintList_addList (ret, | |
1399 | exprNode_traversFalseEnsuresConstraints | |
1400 | (exprData_getCastNode (data) ) ); | |
1401 | break; | |
1402 | ||
9280addf | 1403 | default: |
1404 | break; | |
1405 | } | |
1406 | ||
1407 | return ret; | |
1408 | } | |
1409 | ||
616915dd | 1410 | |
1411 | /* walk down the tree and get all requires Constraints in each subexpression*/ | |
1412 | constraintList exprNode_traversRequiresConstraints (exprNode e) | |
1413 | { | |
470b7798 | 1414 | exprNode t1; |
616915dd | 1415 | |
1416 | bool handledExprNode; | |
1417 | // char * mes; | |
1418 | exprData data; | |
1419 | constraintList ret; | |
1420 | ||
1421 | if (exprNode_handleError (e)) | |
1422 | { | |
c3e695ff | 1423 | ret = constraintList_makeNew(); |
616915dd | 1424 | return ret; |
1425 | } | |
1426 | ret = constraintList_copy (e->requiresConstraints ); | |
1427 | ||
1428 | handledExprNode = TRUE; | |
1429 | ||
1430 | data = e->edata; | |
1431 | ||
1432 | switch (e->kind) | |
1433 | { | |
9280addf | 1434 | case XPR_WHILEPRED: |
1435 | t1 = exprData_getSingle (data); | |
1436 | ret = constraintList_addList ( ret,exprNode_traversRequiresConstraints (t1) ); | |
1437 | break; | |
616915dd | 1438 | |
1439 | case XPR_FETCH: | |
1440 | ||
1441 | ret = constraintList_addList (ret, | |
1442 | exprNode_traversRequiresConstraints | |
1443 | (exprData_getPairA (data) ) ); | |
1444 | ||
1445 | ret = constraintList_addList (ret, | |
1446 | exprNode_traversRequiresConstraints | |
1447 | (exprData_getPairB (data) ) ); | |
1448 | break; | |
1449 | case XPR_PREOP: | |
1450 | ||
1451 | ret = constraintList_addList (ret, | |
1452 | exprNode_traversRequiresConstraints | |
1453 | (exprData_getUopNode (data) ) ); | |
1454 | break; | |
1455 | ||
1456 | case XPR_PARENS: | |
1457 | ret = constraintList_addList (ret, exprNode_traversRequiresConstraints | |
1458 | (exprData_getUopNode (data) ) ); | |
1459 | break; | |
1460 | case XPR_ASSIGN: | |
1461 | ret = constraintList_addList (ret, | |
1462 | exprNode_traversRequiresConstraints | |
1463 | (exprData_getOpA (data) ) ); | |
1464 | ||
1465 | ret = constraintList_addList (ret, | |
1466 | exprNode_traversRequiresConstraints | |
1467 | (exprData_getOpB (data) ) ); | |
1468 | break; | |
1469 | case XPR_OP: | |
1470 | ret = constraintList_addList (ret, | |
1471 | exprNode_traversRequiresConstraints | |
1472 | (exprData_getOpA (data) ) ); | |
1473 | ||
1474 | ret = constraintList_addList (ret, | |
1475 | exprNode_traversRequiresConstraints | |
1476 | (exprData_getOpB (data) ) ); | |
1477 | break; | |
1478 | case XPR_SIZEOFT: | |
1479 | ||
1480 | // ctype_unparse (qtype_getType (exprData_getType (data) ) ); | |
1481 | ||
1482 | break; | |
1483 | ||
1484 | case XPR_SIZEOF: | |
1485 | ||
1486 | ret = constraintList_addList (ret, | |
1487 | exprNode_traversRequiresConstraints | |
1488 | (exprData_getSingle (data) ) ); | |
1489 | break; | |
1490 | ||
1491 | case XPR_CALL: | |
1492 | ret = constraintList_addList (ret, | |
1493 | exprNode_traversRequiresConstraints | |
1494 | (exprData_getFcn (data) ) ); | |
1495 | /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); | |
1496 | break; | |
1497 | ||
1498 | case XPR_RETURN: | |
1499 | ret = constraintList_addList (ret, | |
1500 | exprNode_traversRequiresConstraints | |
1501 | (exprData_getSingle (data) ) ); | |
1502 | break; | |
1503 | ||
1504 | case XPR_NULLRETURN: | |
1505 | // cstring_makeLiteral ("return");; | |
1506 | break; | |
1507 | ||
1508 | case XPR_FACCESS: | |
1509 | ret = constraintList_addList (ret, | |
1510 | exprNode_traversRequiresConstraints | |
1511 | (exprData_getFieldNode (data) ) ); | |
1512 | //exprData_getFieldName (data) ; | |
1513 | break; | |
1514 | ||
1515 | case XPR_ARROW: | |
1516 | ret = constraintList_addList (ret, | |
1517 | exprNode_traversRequiresConstraints | |
1518 | (exprData_getFieldNode (data) ) ); | |
1519 | // exprData_getFieldName (data); | |
1520 | break; | |
1521 | ||
1522 | case XPR_STRINGLITERAL: | |
1523 | // cstring_copy (exprData_getLiteral (data)); | |
1524 | break; | |
1525 | ||
1526 | case XPR_NUMLIT: | |
1527 | // cstring_copy (exprData_getLiteral (data)); | |
1528 | break; | |
1529 | case XPR_POSTOP: | |
1530 | ||
1531 | ret = constraintList_addList (ret, | |
1532 | exprNode_traversRequiresConstraints | |
1533 | (exprData_getUopNode (data) ) ); | |
1534 | break; | |
470b7798 | 1535 | |
1536 | case XPR_CAST: | |
1537 | ||
1538 | ret = constraintList_addList (ret, | |
1539 | exprNode_traversRequiresConstraints | |
1540 | (exprData_getCastNode (data) ) ); | |
1541 | break; | |
1542 | ||
616915dd | 1543 | default: |
1544 | break; | |
1545 | } | |
1546 | ||
1547 | return ret; | |
1548 | } | |
1549 | ||
1550 | ||
1551 | /* walk down the tree and get all Ensures Constraints in each subexpression*/ | |
1552 | constraintList exprNode_traversEnsuresConstraints (exprNode e) | |
1553 | { | |
470b7798 | 1554 | exprNode t1; |
616915dd | 1555 | |
1556 | bool handledExprNode; | |
1557 | // char * mes; | |
1558 | exprData data; | |
1559 | // constraintExpr tmp; | |
1560 | // constraint cons; | |
1561 | constraintList ret; | |
1562 | ||
1563 | ||
1564 | if (exprNode_handleError (e)) | |
1565 | { | |
c3e695ff | 1566 | ret = constraintList_makeNew(); |
616915dd | 1567 | return ret; |
1568 | } | |
1569 | ||
1570 | ret = constraintList_copy (e->ensuresConstraints ); | |
1571 | handledExprNode = TRUE; | |
1572 | ||
1573 | data = e->edata; | |
1574 | ||
1575 | DPRINTF( (message ( | |
1576 | "exprnode_traversEnsuresConstraints call for %s with constraintList of %s", | |
1577 | exprNode_unparse (e), | |
1578 | constraintList_print(e->ensuresConstraints) | |
1579 | ) | |
1580 | )); | |
1581 | ||
1582 | ||
1583 | switch (e->kind) | |
1584 | { | |
9280addf | 1585 | case XPR_WHILEPRED: |
1586 | t1 = exprData_getSingle (data); | |
1587 | ret = constraintList_addList ( ret,exprNode_traversEnsuresConstraints (t1) ); | |
1588 | break; | |
616915dd | 1589 | |
1590 | case XPR_FETCH: | |
1591 | ||
1592 | ret = constraintList_addList (ret, | |
1593 | exprNode_traversEnsuresConstraints | |
1594 | (exprData_getPairA (data) ) ); | |
1595 | ||
1596 | ret = constraintList_addList (ret, | |
1597 | exprNode_traversEnsuresConstraints | |
1598 | (exprData_getPairB (data) ) ); | |
1599 | break; | |
1600 | case XPR_PREOP: | |
1601 | ||
1602 | ret = constraintList_addList (ret, | |
1603 | exprNode_traversEnsuresConstraints | |
1604 | (exprData_getUopNode (data) ) ); | |
1605 | break; | |
1606 | ||
1607 | case XPR_PARENS: | |
1608 | ret = constraintList_addList (ret, exprNode_traversEnsuresConstraints | |
1609 | (exprData_getUopNode (data) ) ); | |
1610 | break; | |
1611 | case XPR_ASSIGN: | |
1612 | ret = constraintList_addList (ret, | |
1613 | exprNode_traversEnsuresConstraints | |
1614 | (exprData_getOpA (data) ) ); | |
1615 | ||
1616 | ret = constraintList_addList (ret, | |
1617 | exprNode_traversEnsuresConstraints | |
1618 | (exprData_getOpB (data) ) ); | |
1619 | break; | |
1620 | case XPR_OP: | |
1621 | ret = constraintList_addList (ret, | |
1622 | exprNode_traversEnsuresConstraints | |
1623 | (exprData_getOpA (data) ) ); | |
1624 | ||
1625 | ret = constraintList_addList (ret, | |
1626 | exprNode_traversEnsuresConstraints | |
1627 | (exprData_getOpB (data) ) ); | |
1628 | break; | |
1629 | case XPR_SIZEOFT: | |
1630 | ||
1631 | // ctype_unparse (qtype_getType (exprData_getType (data) ) ); | |
1632 | ||
1633 | break; | |
1634 | ||
1635 | case XPR_SIZEOF: | |
1636 | ||
1637 | ret = constraintList_addList (ret, | |
1638 | exprNode_traversEnsuresConstraints | |
1639 | (exprData_getSingle (data) ) ); | |
1640 | break; | |
1641 | ||
1642 | case XPR_CALL: | |
1643 | ret = constraintList_addList (ret, | |
1644 | exprNode_traversEnsuresConstraints | |
1645 | (exprData_getFcn (data) ) ); | |
1646 | /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); | |
1647 | break; | |
1648 | ||
1649 | case XPR_RETURN: | |
1650 | ret = constraintList_addList (ret, | |
1651 | exprNode_traversEnsuresConstraints | |
1652 | (exprData_getSingle (data) ) ); | |
1653 | break; | |
1654 | ||
1655 | case XPR_NULLRETURN: | |
1656 | // cstring_makeLiteral ("return");; | |
1657 | break; | |
1658 | ||
1659 | case XPR_FACCESS: | |
1660 | ret = constraintList_addList (ret, | |
1661 | exprNode_traversEnsuresConstraints | |
1662 | (exprData_getFieldNode (data) ) ); | |
1663 | //exprData_getFieldName (data) ; | |
1664 | break; | |
1665 | ||
1666 | case XPR_ARROW: | |
1667 | ret = constraintList_addList (ret, | |
1668 | exprNode_traversEnsuresConstraints | |
1669 | (exprData_getFieldNode (data) ) ); | |
1670 | // exprData_getFieldName (data); | |
1671 | break; | |
1672 | ||
1673 | case XPR_STRINGLITERAL: | |
1674 | // cstring_copy (exprData_getLiteral (data)); | |
1675 | break; | |
1676 | ||
1677 | case XPR_NUMLIT: | |
1678 | // cstring_copy (exprData_getLiteral (data)); | |
1679 | break; | |
1680 | case XPR_POSTOP: | |
1681 | ||
1682 | ret = constraintList_addList (ret, | |
1683 | exprNode_traversEnsuresConstraints | |
1684 | (exprData_getUopNode (data) ) ); | |
1685 | break; | |
470b7798 | 1686 | case XPR_CAST: |
1687 | ||
1688 | ret = constraintList_addList (ret, | |
1689 | exprNode_traversEnsuresConstraints | |
1690 | (exprData_getCastNode (data) ) ); | |
1691 | break; | |
1692 | ||
616915dd | 1693 | default: |
1694 | break; | |
1695 | } | |
1696 | DPRINTF( (message ( | |
1697 | "exprnode_traversEnsuresConstraints call for %s with constraintList of is returning %s", | |
1698 | exprNode_unparse (e), | |
1699 | // constraintList_print(e->ensuresConstraints), | |
1700 | constraintList_print(ret) | |
1701 | ) | |
1702 | )); | |
1703 | ||
1704 | ||
1705 | return ret; | |
1706 | } | |
1707 |