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