]> andersk Git - splint.git/blame - src/constraintGeneration.c
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Fixed bugs in the constant removal code for binary expressions.
[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
7c9c4a67 563static void exprNode_doGenerateConstraintSwitch ( exprNode switchExpr,
564 exprNode body, constraintList * currentRequires, constraintList *
565 currentEnsures, constraintList * savedRequires, constraintList *
566 savedEnsures)
567{
568 exprNode stmt, stmtList;
569
570 DPRINTF(( message("exprNode_doGenerateConstraintSwitch: (switch %s) %s",
571 exprNode_unparse(switchExpr), exprNode_unparse(body)
572 ) ));
573
574 if (exprNode_isError(body) )
575 {
576 return;
577 }
578
579 if (body->kind != XPR_STMTLIST )
580 {
581 DPRINTF((message("exprNode_doGenerateConstraintSwitch: non
582stmtlist: %s",
583 exprNode_unparse(body) )
584 ));
585 // llassert(body->kind == XPR_STMT );
586 stmt = body;
587 stmtList = exprNode_undefined;
588 }
589 else
590 {
591 stmt = exprData_getPairB(body->edata);
592 stmtList = exprData_getPairA(body->edata);
593 }
594
595 DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s
596stmt: %s",
597 exprNode_unparse(stmtList), exprNode_unparse(stmt) )
598 ));
599
600
601 exprNode_doGenerateConstraintSwitch (switchExpr, stmtList, currentRequires, currentEnsures,
602 savedRequires, savedEnsures );
603
604 if (exprNode_isError(stmt) )
605 return;
606
607 exprNode_stmt(stmt);
608 //, FALSE, FALSE, exprNode_getfileloc(stmt) );
609
610 if (! exprNode_isCaseMarker(stmt) )
611 {
612
613 constraintList temp;
614
615 DPRINTF (( message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt),
616 constraintList_unparse(stmt->requiresConstraints), constraintList_unparse(stmt->ensuresConstraints) ) ));
617
618 temp = constraintList_reflectChanges (stmt->requiresConstraints,
619 *currentEnsures);
620
621 *currentRequires = constraintList_mergeRequiresFreeFirst
622 (*currentRequires,
623 temp);
624
625 constraintList_free(temp);
626
627 *currentEnsures = constraintList_mergeEnsuresFreeFirst
628 (*currentEnsures,
629 stmt->ensuresConstraints);
630 DPRINTF(( message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
631 "%s currentEnsures:%s",
632 exprNode_unparse(switchExpr), exprNode_unparse(body),
633 constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
634 ) ));
635 return;
636 }
637
638 if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList) )
639 {
640 // merge current and saved constraint with Logical Or...
641 // make a constraint for ensures
642
643 constraintList temp;
644 constraint con;
645
646 DPRINTF (( message("Got case marker") ));
647
648 if (constraintList_isUndefined(*savedEnsures) &&
649 constraintList_isUndefined(*savedRequires) )
650 {
651 *savedEnsures = constraintList_copy(*currentEnsures);
652 *savedRequires = constraintList_copy(*currentRequires);
653 }
654 else
655 {
656 DPRINTF (( message("Doing logical or") ));
657 temp = constraintList_logicalOr (*savedEnsures, *currentEnsures);
658 constraintList_free (*savedEnsures);
659 *savedEnsures = temp;
660
661 *savedRequires = constraintList_mergeRequiresFreeFirst (*savedRequires, *currentRequires);
662 }
663
664 con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
665 (stmt->edata), exprNode_getfileloc(stmt) );
666
667
668 constraintList_free(*currentEnsures);
669 *currentEnsures = constraintList_makeNew();
670 *currentEnsures = constraintList_add(*currentEnsures, con);
671
672 constraintList_free(*currentRequires);
673 *currentRequires = constraintList_makeNew();
674 DPRINTF(( message("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:"
675 "%s savedEnsures:%s",
676 exprNode_unparse(switchExpr), exprNode_unparse(body),
677 constraintList_print(*savedRequires), constraintList_print(*savedEnsures)
678 ) ));
679
680 }
681
682 else if (exprNode_isCaseMarker(stmt) )
683 //prior case has no break.
684 {
685 // We don't do anything to the sved constraints because the case hasn't ended
686 //The new ensures constraints for the case will be:
687 // the constraint for the case statement (CASE_LABEL == SWITCH_EXPR) logicalOr currentEnsures
688
689 constraintList temp;
690 constraint con;
691
692 constraintList ensuresTemp;
693
694 DPRINTF (( message("Got case marker with no prior break") ));
695
696 con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
697 (stmt->edata), exprNode_getfileloc(stmt) );
698
699 ensuresTemp = constraintList_makeNew();
700
701 ensuresTemp = constraintList_add (ensuresTemp, con);
702
703 if (exprNode_isError(stmtList) )
704 {
705 constraintList_free(*currentEnsures);
706 *currentEnsures = constraintList_copy(ensuresTemp);
707 }
708 else
709 {
710
711 temp = constraintList_logicalOr (*currentEnsures, ensuresTemp);
712
713 constraintList_free(*currentEnsures);
714 constraintList_free(ensuresTemp);
715
716 *currentEnsures = temp;
717 }
718 constraintList_free(*currentRequires);
719
720 *currentRequires = constraintList_makeNew();
721 }
722
723 DPRINTF(( message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
724 "%s currentEnsures:%s",
725 exprNode_unparse(switchExpr), exprNode_unparse(body),
726 constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
727 ) ));
728 return;
729
730}
731
732
733static void exprNode_generateConstraintSwitch ( exprNode switchStmt)
734{
735 constraintList constraintsRequires;
736 constraintList constraintsEnsures;
737 constraintList lastRequires;
738 constraintList lastEnsures;
739
740 exprNode body;
741 exprNode switchExpr;
742
743 switchExpr = exprData_getPairA(switchStmt->edata);
744 body = exprData_getPairB(switchStmt->edata);
745
746 //*@i22*/
747 if ( body->kind == XPR_BLOCK)
748 body = exprData_getSingle(body->edata);
749
750 constraintsRequires = constraintList_undefined;
751 constraintsEnsures = constraintList_undefined;
752
753 lastRequires = constraintList_makeNew();
754 lastEnsures = constraintList_makeNew();
755
756
757 exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires, &lastEnsures, &constraintsRequires, &constraintsEnsures);
758
759 // merge current and saved constraint with Logical Or...
760 // make a constraint for ensures
761
762 constraintList_free(switchStmt->requiresConstraints);
763 constraintList_free(switchStmt->ensuresConstraints);
764
765 if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires) )
766 {
767 switchStmt->ensuresConstraints = constraintList_logicalOr(constraintsEnsures, lastEnsures);
768 switchStmt->requiresConstraints = constraintList_mergeRequires(constraintsRequires, lastRequires);
769 constraintList_free (constraintsRequires);
770 constraintList_free (constraintsEnsures);
771 }
772 else
773 {
774 switchStmt->ensuresConstraints = constraintList_copy(lastEnsures);
775 switchStmt->requiresConstraints = constraintList_copy(lastRequires);
776 }
777
778 constraintList_free (lastRequires);
779 constraintList_free (lastEnsures);
780
781 DPRINTF(( (message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s",
782 constraintList_print( switchStmt->requiresConstraints),
783 constraintList_print( switchStmt->ensuresConstraints)
784 )
785 ) ));
786}
787
bb25bea6 788static exprNode doSwitch (/*@returned@*/ exprNode e)
470b7798 789{
790 exprNode body;
791 exprData data;
792
793 data = e->edata;
2681ee39 794 // llassert(FALSE);
7c9c4a67 795 DPRINTF (( message ("doSwitch for: switch (%s) %s",
2681ee39 796 exprNode_unparse (exprData_getPairA (data)),
797 exprNode_unparse (exprData_getPairB (data))) ));
7c9c4a67 798
470b7798 799 body = exprData_getPairB (data);
7c9c4a67 800
2681ee39 801 exprNode_generateConstraints(body);
2681ee39 802
7c9c4a67 803 exprNode_generateConstraintSwitch (e);
804
805 // e->requiresConstraints = constraintList_copy (body->requiresConstraints );
806 // e->ensuresConstraints = constraintList_copy (body->ensuresConstraints );
807
470b7798 808 return e;
809}
9280addf 810
811
7c9c4a67 812
813
28bf4b0b 814void exprNode_multiStatement (/*@dependent@*/ exprNode e)
616915dd 815{
816
817 bool ret;
818 exprData data;
819 exprNode e1, e2;
820 exprNode p, trueBranch, falseBranch;
821 exprNode forPred, forBody;
470b7798 822 exprNode test;
bb25bea6 823
824 constraintList temp;
825
470b7798 826 // constraintList t, f;
bb25bea6 827 /*e->requiresConstraints = constraintList_makeNew();
c3e695ff 828 e->ensuresConstraints = constraintList_makeNew();
829 e->trueEnsuresConstraints = constraintList_makeNew();
830 e->falseEnsuresConstraints = constraintList_makeNew();
bb25bea6 831 */
616915dd 832 // e = makeDataTypeConstraints(e);
833
834 DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
835 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
836
837 if (exprNode_handleError (e))
838 {
84c9ffbf 839 return; // FALSE;
616915dd 840 }
841
842 data = e->edata;
843
844 ret = TRUE;
845
846 switch (e->kind)
847 {
848
849 case XPR_FOR:
850 // ret = message ("%s %s",
851 forPred = exprData_getPairA (data);
852 forBody = exprData_getPairB (data);
853
854 //first generate the constraints
855 exprNode_generateConstraints (forPred);
856 exprNode_generateConstraints (forBody);
857
858
859 doFor (e, forPred, forBody);
860
861 break;
862
863 case XPR_FORPRED:
864 // ret = message ("for (%s; %s; %s)",
865 exprNode_generateConstraints (exprData_getTripleInit (data) );
866 test = exprData_getTripleTest (data);
867 exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
9280addf 868 exprNode_generateConstraints (exprData_getTripleInc (data) );
869
616915dd 870 if (!exprNode_isError(test) )
bb25bea6 871 {
872 constraintList temp2;
873 temp2 = test->trueEnsuresConstraints;
874 test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
875 constraintList_free(temp2);
876 }
877
616915dd 878 exprNode_generateConstraints (exprData_getTripleInc (data));
879 break;
9280addf 880
881 case XPR_WHILE:
882 e1 = exprData_getPairA (data);
883 e2 = exprData_getPairB (data);
884
885 exprNode_exprTraverse (e1,
886 FALSE, FALSE, exprNode_loc(e1));
887
888 exprNode_generateConstraints (e2);
889
890 e = doWhile (e, e1, e2);
891
892 break;
893
616915dd 894 case XPR_IF:
895 DPRINTF(( "IF:") );
896 DPRINTF ((exprNode_unparse(e) ) );
897 // ret = message ("if (%s) %s",
898 e1 = exprData_getPairA (data);
899 e2 = exprData_getPairB (data);
900
901 exprNode_exprTraverse (e1,
902 FALSE, FALSE, exprNode_loc(e1));
903
904 exprNode_generateConstraints (e2);
616915dd 905 e = doIf (e, e1, e2);
906
907
908 // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
909 break;
9280addf 910
911
616915dd 912 case XPR_IFELSE:
913 DPRINTF(("Starting IFELSE"));
914 // ret = message ("if (%s) %s else %s",
915 p = exprData_getTriplePred (data);
916 trueBranch = exprData_getTripleTrue (data);
917 falseBranch = exprData_getTripleFalse (data);
918
919 exprNode_exprTraverse (p,
920 FALSE, FALSE, exprNode_loc(p));
921 exprNode_generateConstraints (trueBranch);
922 exprNode_generateConstraints (falseBranch);
923
bb25bea6 924 temp = p->ensuresConstraints;
9280addf 925 p->ensuresConstraints = exprNode_traversEnsuresConstraints (p);
bb25bea6 926 constraintList_free(temp);
927
928 temp = p->requiresConstraints;
470b7798 929 p->requiresConstraints = exprNode_traversRequiresConstraints (p);
bb25bea6 930 constraintList_free(temp);
931
932 temp = p->trueEnsuresConstraints;
9280addf 933 p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p);
bb25bea6 934 constraintList_free(temp);
935
936 temp = p->falseEnsuresConstraints;
470b7798 937 p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p);
bb25bea6 938 constraintList_free(temp);
616915dd 939
470b7798 940 e = doIfElse (e, p, trueBranch, falseBranch);
616915dd 941 DPRINTF( ("Done IFELSE") );
942 break;
9280addf 943
616915dd 944 case XPR_DOWHILE:
470b7798 945
946 e2 = (exprData_getPairB (data));
947 e1 = (exprData_getPairA (data));
948
949 DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1) ) ));
950 exprNode_generateConstraints (e2);
951 exprNode_generateConstraints (e1);
952 e = exprNode_copyConstraints (e, e2);
953 DPRINTF ((message ("e = %s ", constraintList_print(e->requiresConstraints) ) ));
954
616915dd 955 break;
956
957 case XPR_BLOCK:
958 // ret = message ("{ %s }",
959 exprNode_generateConstraints (exprData_getSingle (data));
bb25bea6 960
961 constraintList_free(e->requiresConstraints);
616915dd 962 e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
bb25bea6 963
964 constraintList_free(e->ensuresConstraints);
616915dd 965 e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
966 // e->constraints = (exprData_getSingle (data))->constraints;
967 break;
968
470b7798 969 case XPR_SWITCH:
970 e = doSwitch (e);
971 break;
616915dd 972 case XPR_STMT:
973 case XPR_STMTLIST:
84c9ffbf 974 exprNode_stmtList (e);
975 return ;
616915dd 976 /*@notreached@*/
977 break;
978 default:
979 ret=FALSE;
980 }
84c9ffbf 981 return; // ret;
616915dd 982}
983
bb25bea6 984static bool lltok_isBoolean_Op (lltok tok)
616915dd 985{
986 /*this should really be a switch statement but
987 I don't want to violate the abstraction
988 maybe this should go in lltok.c */
989
990 if (lltok_isEq_Op (tok) )
991 {
992 return TRUE;
993 }
994 if (lltok_isAnd_Op (tok) )
995
996 {
997
998 return TRUE;
999 }
1000 if (lltok_isOr_Op (tok) )
1001 {
1002 return TRUE;
1003 }
1004
1005 if (lltok_isGt_Op (tok) )
1006 {
1007 return TRUE;
1008 }
1009 if (lltok_isLt_Op (tok) )
1010 {
1011 return TRUE;
1012 }
1013
1014 if (lltok_isLe_Op (tok) )
1015 {
1016 return TRUE;
1017 }
1018
1019 if (lltok_isGe_Op (tok) )
1020 {
1021 return TRUE;
1022 }
1023
1024 return FALSE;
1025
1026}
1027
1028
28bf4b0b 1029static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv, fileloc sequencePoint)
616915dd 1030{
1031 constraint cons;
1032exprNode t1, t2;
1033exprData data;
1034lltok tok;
bb25bea6 1035constraintList tempList, temp;
616915dd 1036data = e->edata;
1037
1038tok = exprData_getOpTok (data);
1039
1040
1041t1 = exprData_getOpA (data);
1042t2 = exprData_getOpB (data);
1043
1044
920a3797 1045 tempList = constraintList_undefined;
1046
616915dd 1047/* arithmetic tests */
1048
1049if (lltok_isEq_Op (tok) )
1050{
1051 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
1052 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1053}
1054
1055
1056 if (lltok_isLt_Op (tok) )
1057 {
1058 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1059 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1060 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1061 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1062 }
1063
1064
1065if (lltok_isGe_Op (tok) )
1066{
1067
1068 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1069 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1070
1071 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1072 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1073
1074}
1075
1076
1077 if (lltok_isGt_Op (tok) )
1078{
1079 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1080 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1081 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1082 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1083}
1084
1085if (lltok_isLe_Op (tok) )
1086{
1087 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1088 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1089
1090 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1091 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1092}
1093
1094
1095
1096/*Logical operations */
1097
920a3797 1098
616915dd 1099 if (lltok_isAnd_Op (tok) )
1100
1101 {
1102 //true ensures
1103 tempList = constraintList_copy (t1->trueEnsuresConstraints);
1104 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
4ab867d6 1105 e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
616915dd 1106
1107 //false ensures: fens t1 or tens t1 and fens t2
1108 tempList = constraintList_copy (t1->trueEnsuresConstraints);
1109 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
bb25bea6 1110 temp = tempList;
616915dd 1111 tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
60eced23 1112 constraintList_free (temp);
1113
1114 /* evans - was constraintList_addList - memory leak detected by lclint */
1115 e->falseEnsuresConstraints =constraintList_addListFree (e->falseEnsuresConstraints, tempList);
616915dd 1116 }
84c9ffbf 1117 else if (lltok_isOr_Op (tok) )
1118 {
616915dd 1119 //false ensures
1120 tempList = constraintList_copy (t1->falseEnsuresConstraints);
1121 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
4ab867d6 1122 e->falseEnsuresConstraints = constraintList_addListFree(e->falseEnsuresConstraints, tempList);
616915dd 1123
1124 //true ensures: tens t1 or fens t1 and tens t2
1125 tempList = constraintList_copy (t1->falseEnsuresConstraints);
1126 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
bb25bea6 1127
1128 temp = tempList;
616915dd 1129 tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
bb25bea6 1130 constraintList_free(temp);
1131
60eced23 1132 e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
920a3797 1133 tempList = constraintList_undefined;
616915dd 1134 }
84c9ffbf 1135 else
1136 {
1137 DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok) ) ));
60eced23 1138 }
616915dd 1139}
1140
28bf4b0b 1141void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
616915dd 1142{
9280addf 1143 exprNode t1, t2, fcn;
616915dd 1144 lltok tok;
1145 bool handledExprNode;
1146 exprData data;
1147 constraint cons;
1148
bb25bea6 1149 constraintList temp;
1150
470b7798 1151 if (exprNode_isError(e) )
1152 {
84c9ffbf 1153 return; // FALSE;
470b7798 1154 }
1155
1156 DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
616915dd 1157 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
470b7798 1158
bb25bea6 1159 /*e->requiresConstraints = constraintList_makeNew();
c3e695ff 1160 e->ensuresConstraints = constraintList_makeNew();
1161 e->trueEnsuresConstraints = constraintList_makeNew();;
1162 e->falseEnsuresConstraints = constraintList_makeNew();;
bb25bea6 1163 */
470b7798 1164 if (exprNode_isUnhandled (e) )
616915dd 1165 {
84c9ffbf 1166 return; // FALSE;
616915dd 1167 }
1168 // e = makeDataTypeConstraints (e);
1169
1170 handledExprNode = TRUE;
1171
1172 data = e->edata;
1173
1174 switch (e->kind)
1175 {
616915dd 1176 case XPR_WHILEPRED:
1177 t1 = exprData_getSingle (data);
1178 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
1179 e = exprNode_copyConstraints (e, t1);
1180 break;
1181
1182 case XPR_FETCH:
1183
1184 if (definatelv )
1185 {
1186 t1 = (exprData_getPairA (data) );
1187 t2 = (exprData_getPairB (data) );
1188 cons = constraint_makeWriteSafeExprNode (t1, t2);
1189 }
1190 else
1191 {
1192 t1 = (exprData_getPairA (data) );
1193 t2 = (exprData_getPairB (data) );
1194 cons = constraint_makeReadSafeExprNode (t1, t2 );
1195 }
1196
1197 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1198 cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
1199 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1200
9280addf 1201 cons = constraint_makeEnsureLteMaxRead (t2, t1);
616915dd 1202 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1203
1204 // cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
1205 // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
d46ce6a4 1206
616915dd 1207 exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
1208 exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
1209
1210 /*@i325 Should check which is array/index. */
1211 break;
1212
1213 case XPR_PARENS:
1214 exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
1215 // e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
1216 break;
1217 case XPR_INIT:
920a3797 1218 {
1219 /*
1220 idDecl t;
1221
1222 uentry ue;
1223 exprNode lhs;
1224
1225 t = exprData_getInitId (data);
1226 ue = usymtab_lookup (idDecl_observeId (t));
1227 lhs = exprNode_createId (ue);
1228 */
1229 t2 = exprData_getInitNode (data);
1230
1231 /* DPRINTF(( (message("initialization: %s = %s",
1232 exprNode_unparse(lhs),
1233 exprNode_unparse(t2)
1234 )
1235 ) )); */
1236
1237 //exprNode_exprTraverse (t1, TRUE, FALSE, sequencePoint );
1238
1239 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1240
1241 /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
616915dd 1242 if ( (!exprNode_isError (e)) && (!exprNode_isError(t2)) )
920a3797 1243 {
1244 cons = constraint_makeEnsureEqual (e, t2, sequencePoint);
1245 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1246 }
1247 }
616915dd 1248
1249 break;
1250 case XPR_ASSIGN:
1251 t1 = exprData_getOpA (data);
1252 t2 = exprData_getOpB (data);
1253 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
84c9ffbf 1254 //lltok_unparse (exprData_getOpTok (data));
920a3797 1255
616915dd 1256 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1257
1258 /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
1259 if ( (!exprNode_isError (t1)) && (!exprNode_isError(t2)) )
1260 {
1261 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
1262 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1263 }
1264 break;
1265 case XPR_OP:
1266 t1 = exprData_getOpA (data);
1267 t2 = exprData_getOpB (data);
616915dd 1268 tok = exprData_getOpTok (data);
2934b455 1269
920a3797 1270
2934b455 1271 if (tok.tok == ADD_ASSIGN)
1272 {
920a3797 1273 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1274 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1275
2934b455 1276 cons = constraint_makeAddAssign (t1, t2, sequencePoint );
1277 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1278 }
920a3797 1279 else if (tok.tok == SUB_ASSIGN)
2934b455 1280 {
920a3797 1281 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1282 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1283
2934b455 1284 cons = constraint_makeSubtractAssign (t1, t2, sequencePoint );
1285 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1286 }
920a3797 1287 else
1288 {
1289 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
1290 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1291 }
2934b455 1292
616915dd 1293 if (lltok_isBoolean_Op (tok) )
1294 exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
1295
1296 // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
1297 break;
1298 case XPR_SIZEOFT:
28bf4b0b 1299 //drl possible problem : warning make sure the case can be ignored..
616915dd 1300
1301 break;
1302
1303 case XPR_SIZEOF:
1304 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
1305 // e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
1306 break;
1307
1308 case XPR_CALL:
9280addf 1309 fcn = exprData_getFcn(data);
1310
1311 exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint );
9280addf 1312 DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data) ) ) ) );
616915dd 1313
4ab867d6 1314 fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
9280addf 1315 checkCall (fcn, exprData_getArgs (data) ) );
616915dd 1316
4ab867d6 1317 fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints,
28bf4b0b 1318 exprNode_getPostConditions(fcn, exprData_getArgs (data),e ) );
9280addf 1319
1320 t1 = exprNode_createNew (exprNode_getType (e) );
1321
1322 checkArgumentList (t1, exprData_getArgs(data), sequencePoint);
616915dd 1323
9280addf 1324
28bf4b0b 1325 exprNode_mergeResolve (e, t1, fcn);
920a3797 1326
1327 exprNode_free(t1);
9280addf 1328
616915dd 1329 // e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) );
920a3797 1330
616915dd 1331 break;
1332
1333 case XPR_RETURN:
1334 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
1335 break;
1336
1337 case XPR_NULLRETURN:
84c9ffbf 1338
616915dd 1339 break;
1340
1341
1342 case XPR_FACCESS:
1343 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
616915dd 1344 break;
1345
1346 case XPR_ARROW:
1347 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
616915dd 1348 break;
1349
1350 case XPR_STRINGLITERAL:
84c9ffbf 1351
616915dd 1352 break;
1353
1354 case XPR_NUMLIT:
84c9ffbf 1355
616915dd 1356 break;
1357
1358 case XPR_PREOP:
1359 t1 = exprData_getUopNode(data);
1360 tok = (exprData_getUopTok (data));
1361 //lltok_unparse (exprData_getUopTok (data));
1362 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
1363 /*handle * pointer access */
1364 if (lltok_isInc_Op (tok) )
1365 {
1366 DPRINTF(("doing ++(var)"));
1367 t1 = exprData_getUopNode (data);
1368 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
1369 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1370 }
1371 else if (lltok_isDec_Op (tok) )
1372 {
1373 DPRINTF(("doing --(var)"));
1374 t1 = exprData_getUopNode (data);
1375 cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1376 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1377 }
84c9ffbf 1378 else if (lltok_isMult( tok ) )
616915dd 1379 {
1380 if (definatelv)
1381 {
1382 cons = constraint_makeWriteSafeInt (t1, 0);
1383 }
1384 else
1385 {
1386 cons = constraint_makeReadSafeInt (t1, 0);
1387 }
1388 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1389 }
84c9ffbf 1390 else if (lltok_isNot_Op (tok) )
1391 /* ! expr */
616915dd 1392 {
bb25bea6 1393 constraintList_free(e->trueEnsuresConstraints);
1394
616915dd 1395 e->trueEnsuresConstraints = constraintList_copy (t1->falseEnsuresConstraints);
bb25bea6 1396 constraintList_free(e->falseEnsuresConstraints);
616915dd 1397 e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
1398 }
bb25bea6 1399
84c9ffbf 1400 else if (lltok_isAmpersand_Op (tok) )
1401 {
1402 break;
1403 }
bb25bea6 1404 else if (lltok_isMinus_Op (tok) )
1405 {
1406 break;
1407 }
4ab867d6 1408 else if ( lltok_isExcl_Op (tok) )
1409 {
1410 break;
1411 }
1412 else if (lltok_isTilde_Op (tok) )
1413 {
1414 break;
1415 }
84c9ffbf 1416 else
1417 {
1418 llcontbug((message("Unsupported preop in %s", exprNode_unparse(e) ) ));
1419 BADEXIT;
1420 }
616915dd 1421 break;
1422
1423 case XPR_POSTOP:
1424
1425 exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
84c9ffbf 1426
616915dd 1427 if (lltok_isInc_Op (exprData_getUopTok (data) ) )
1428 {
1429 DPRINTF(("doing ++"));
1430 t1 = exprData_getUopNode (data);
1431 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
1432 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1433 }
1434 if (lltok_isDec_Op (exprData_getUopTok (data) ) )
1435 {
1436 DPRINTF(("doing --"));
1437 t1 = exprData_getUopNode (data);
1438 cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1439 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1440 }
1441 break;
470b7798 1442 case XPR_CAST:
920a3797 1443 {
1444 t2 = exprData_getCastNode (data);
1445 DPRINTF (( message ("Examining cast (%q)%s",
1446 qtype_unparse (exprData_getCastType (data)),
1447 exprNode_unparse (t2) )
1448 ));
1449 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1450 }
470b7798 1451 break;
920a3797 1452
470b7798 1453 case XPR_COND:
1454 {
28bf4b0b 1455 exprNode pred, trueBranch, falseBranch;
470b7798 1456 llassert(FALSE);
1457 pred = exprData_getTriplePred (data);
28bf4b0b 1458 trueBranch = exprData_getTripleTrue (data);
1459 falseBranch = exprData_getTripleFalse (data);
470b7798 1460
1461 exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint );
bb25bea6 1462
1463 temp = pred->ensuresConstraints;
470b7798 1464 pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
bb25bea6 1465 constraintList_free(temp);
1466
1467 temp = pred->requiresConstraints;
470b7798 1468 pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
bb25bea6 1469 constraintList_free(temp);
470b7798 1470
bb25bea6 1471 temp = pred->trueEnsuresConstraints;
470b7798 1472 pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred);
bb25bea6 1473 constraintList_free(temp);
1474
1475 temp = pred->falseEnsuresConstraints;
470b7798 1476 pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
bb25bea6 1477 constraintList_free(temp);
1478
470b7798 1479
28bf4b0b 1480 exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint );
bb25bea6 1481
28bf4b0b 1482 temp = trueBranch->ensuresConstraints;
1483 trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
bb25bea6 1484 constraintList_free(temp);
1485
1486
28bf4b0b 1487 temp = trueBranch->requiresConstraints;
1488 trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
bb25bea6 1489 constraintList_free(temp);
1490
470b7798 1491
28bf4b0b 1492 temp = trueBranch->trueEnsuresConstraints;
1493 trueBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(trueBranch);
bb25bea6 1494 constraintList_free(temp);
1495
28bf4b0b 1496 temp = trueBranch->falseEnsuresConstraints;
1497 trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
bb25bea6 1498 constraintList_free(temp);
470b7798 1499
bb25bea6 1500 //dfdf
28bf4b0b 1501 exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint );
bb25bea6 1502
28bf4b0b 1503 temp = falseBranch->ensuresConstraints;
1504 falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
bb25bea6 1505 constraintList_free(temp);
1506
1507
28bf4b0b 1508 temp = falseBranch->requiresConstraints;
1509 falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
bb25bea6 1510 constraintList_free(temp);
1511
470b7798 1512
28bf4b0b 1513 temp = falseBranch->trueEnsuresConstraints;
1514 falseBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(falseBranch);
bb25bea6 1515 constraintList_free(temp);
470b7798 1516
28bf4b0b 1517 temp = falseBranch->falseEnsuresConstraints;
1518 falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
bb25bea6 1519 constraintList_free(temp);
470b7798 1520
1521 /* if pred is true e equals true otherwise pred equals false */
1522
28bf4b0b 1523 cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1524 trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
470b7798 1525
28bf4b0b 1526 cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1527 falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
470b7798 1528
28bf4b0b 1529 e = doIfElse (e, pred, trueBranch, falseBranch);
470b7798 1530
1531 }
1532 break;
1533 case XPR_COMMA:
1534 llassert(FALSE);
1535 t1 = exprData_getPairA (data);
1536 t2 = exprData_getPairB (data);
1537 /* we essiantially treat this like expr1; expr2
1538 of course sequencePoint isn't adjusted so this isn't completely accurate
1539 problems../ */
1540 exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint );
1541 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
28bf4b0b 1542 exprNode_mergeResolve (e, t1, t2);
470b7798 1543 break;
920a3797 1544
616915dd 1545 default:
1546 handledExprNode = FALSE;
1547 }
1548
1549 e->requiresConstraints = constraintList_preserveOrig ( e->requiresConstraints);
1550 e->ensuresConstraints = constraintList_preserveOrig ( e->ensuresConstraints);
9280addf 1551 e->requiresConstraints = constraintList_addGeneratingExpr ( e->requiresConstraints, e);
1552
1553 e->ensuresConstraints = constraintList_addGeneratingExpr ( e->ensuresConstraints, e);
1554
d46ce6a4 1555 DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
1556
1557 DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
616915dd 1558
bb25bea6 1559 DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints) ) ));
1560
1561 DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) ));
1562
84c9ffbf 1563 return; // handledExprNode;
616915dd 1564}
1565
1566
1567constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
1568{
470b7798 1569 exprNode t1;
616915dd 1570
1571 bool handledExprNode;
1572 // char * mes;
1573 exprData data;
1574 constraintList ret;
1575
2681ee39 1576 if (exprNode_handleError (e))
1577 {
1578 ret = constraintList_makeNew();
1579 return ret;
1580 }
616915dd 1581 ret = constraintList_copy (e->trueEnsuresConstraints );
1582
2681ee39 1583 handledExprNode = TRUE;
616915dd 1584
1585 data = e->edata;
1586
1587 switch (e->kind)
1588 {
9280addf 1589 case XPR_WHILEPRED:
1590 t1 = exprData_getSingle (data);
4ab867d6 1591 ret = constraintList_addListFree ( ret, exprNode_traversTrueEnsuresConstraints (t1) );
9280addf 1592 break;
616915dd 1593
1594 case XPR_FETCH:
1595
4ab867d6 1596 ret = constraintList_addListFree (ret,
616915dd 1597 exprNode_traversTrueEnsuresConstraints
1598 (exprData_getPairA (data) ) );
1599
4ab867d6 1600 ret = constraintList_addListFree (ret,
616915dd 1601 exprNode_traversTrueEnsuresConstraints
1602 (exprData_getPairB (data) ) );
1603 break;
1604 case XPR_PREOP:
1605
4ab867d6 1606 ret = constraintList_addListFree (ret,
616915dd 1607 exprNode_traversTrueEnsuresConstraints
1608 (exprData_getUopNode (data) ) );
1609 break;
1610
1611 case XPR_PARENS:
4ab867d6 1612 ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
616915dd 1613 (exprData_getUopNode (data) ) );
1614 break;
2681ee39 1615
1616 case XPR_INIT:
1617 ret = constraintList_addListFree (ret,
1618 exprNode_traversTrueEnsuresConstraints
1619 (exprData_getInitNode (data) ) );
1620 break;
1621
1622
616915dd 1623 case XPR_ASSIGN:
4ab867d6 1624 ret = constraintList_addListFree (ret,
616915dd 1625 exprNode_traversTrueEnsuresConstraints
1626 (exprData_getOpA (data) ) );
1627
4ab867d6 1628 ret = constraintList_addListFree (ret,
616915dd 1629 exprNode_traversTrueEnsuresConstraints
1630 (exprData_getOpB (data) ) );
1631 break;
1632 case XPR_OP:
4ab867d6 1633 ret = constraintList_addListFree (ret,
616915dd 1634 exprNode_traversTrueEnsuresConstraints
1635 (exprData_getOpA (data) ) );
1636
4ab867d6 1637 ret = constraintList_addListFree (ret,
616915dd 1638 exprNode_traversTrueEnsuresConstraints
1639 (exprData_getOpB (data) ) );
1640 break;
1641 case XPR_SIZEOFT:
1642
1643 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1644
1645 break;
1646
1647 case XPR_SIZEOF:
1648
4ab867d6 1649 ret = constraintList_addListFree (ret,
1650 exprNode_traversTrueEnsuresConstraints
1651 (exprData_getSingle (data) ) );
616915dd 1652 break;
1653
1654 case XPR_CALL:
4ab867d6 1655 ret = constraintList_addListFree (ret,
616915dd 1656 exprNode_traversTrueEnsuresConstraints
1657 (exprData_getFcn (data) ) );
1658 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1659 break;
1660
1661 case XPR_RETURN:
4ab867d6 1662 ret = constraintList_addListFree (ret,
616915dd 1663 exprNode_traversTrueEnsuresConstraints
1664 (exprData_getSingle (data) ) );
1665 break;
1666
1667 case XPR_NULLRETURN:
1668 // cstring_makeLiteral ("return");;
1669 break;
1670
1671 case XPR_FACCESS:
4ab867d6 1672 ret = constraintList_addListFree (ret,
616915dd 1673 exprNode_traversTrueEnsuresConstraints
1674 (exprData_getFieldNode (data) ) );
1675 //exprData_getFieldName (data) ;
1676 break;
1677
1678 case XPR_ARROW:
4ab867d6 1679 ret = constraintList_addListFree (ret,
616915dd 1680 exprNode_traversTrueEnsuresConstraints
1681 (exprData_getFieldNode (data) ) );
1682 // exprData_getFieldName (data);
1683 break;
1684
1685 case XPR_STRINGLITERAL:
1686 // cstring_copy (exprData_getLiteral (data));
1687 break;
1688
1689 case XPR_NUMLIT:
1690 // cstring_copy (exprData_getLiteral (data));
1691 break;
1692 case XPR_POSTOP:
1693
4ab867d6 1694 ret = constraintList_addListFree (ret,
616915dd 1695 exprNode_traversTrueEnsuresConstraints
1696 (exprData_getUopNode (data) ) );
1697 break;
470b7798 1698
1699 case XPR_CAST:
1700
4ab867d6 1701 ret = constraintList_addListFree (ret,
470b7798 1702 exprNode_traversTrueEnsuresConstraints
1703 (exprData_getCastNode (data) ) );
470b7798 1704 break;
84c9ffbf 1705
616915dd 1706 default:
1707 break;
1708 }
1709
1710 return ret;
1711}
1712
9280addf 1713constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
1714{
470b7798 1715 exprNode t1;
9280addf 1716
1717 bool handledExprNode;
1718 // char * mes;
1719 exprData data;
1720 constraintList ret;
1721
1722 if (exprNode_handleError (e))
1723 {
c3e695ff 1724 ret = constraintList_makeNew();
9280addf 1725 return ret;
1726 }
1727 ret = constraintList_copy (e->falseEnsuresConstraints );
1728
1729 handledExprNode = TRUE;
1730
1731 data = e->edata;
1732
1733 switch (e->kind)
1734 {
1735 case XPR_WHILEPRED:
1736 t1 = exprData_getSingle (data);
4ab867d6 1737 ret = constraintList_addListFree ( ret,exprNode_traversFalseEnsuresConstraints (t1) );
9280addf 1738 break;
1739
1740 case XPR_FETCH:
1741
4ab867d6 1742 ret = constraintList_addListFree (ret,
9280addf 1743 exprNode_traversFalseEnsuresConstraints
1744 (exprData_getPairA (data) ) );
1745
4ab867d6 1746 ret = constraintList_addListFree (ret,
9280addf 1747 exprNode_traversFalseEnsuresConstraints
1748 (exprData_getPairB (data) ) );
1749 break;
1750 case XPR_PREOP:
1751
4ab867d6 1752 ret = constraintList_addListFree (ret,
9280addf 1753 exprNode_traversFalseEnsuresConstraints
1754 (exprData_getUopNode (data) ) );
1755 break;
1756
1757 case XPR_PARENS:
4ab867d6 1758 ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
9280addf 1759 (exprData_getUopNode (data) ) );
1760 break;
2681ee39 1761 case XPR_INIT:
1762 ret = constraintList_addListFree (ret,
1763 exprNode_traversFalseEnsuresConstraints
1764 ( exprData_getInitNode (data) ) );
1765 break;
1766
9280addf 1767 case XPR_ASSIGN:
4ab867d6 1768 ret = constraintList_addListFree (ret,
9280addf 1769 exprNode_traversFalseEnsuresConstraints
1770 (exprData_getOpA (data) ) );
1771
4ab867d6 1772 ret = constraintList_addListFree (ret,
9280addf 1773 exprNode_traversFalseEnsuresConstraints
1774 (exprData_getOpB (data) ) );
1775 break;
1776 case XPR_OP:
4ab867d6 1777 ret = constraintList_addListFree (ret,
9280addf 1778 exprNode_traversFalseEnsuresConstraints
1779 (exprData_getOpA (data) ) );
1780
4ab867d6 1781 ret = constraintList_addListFree (ret,
9280addf 1782 exprNode_traversFalseEnsuresConstraints
1783 (exprData_getOpB (data) ) );
1784 break;
1785 case XPR_SIZEOFT:
1786
1787 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1788
1789 break;
1790
1791 case XPR_SIZEOF:
1792
4ab867d6 1793 ret = constraintList_addListFree (ret,
9280addf 1794 exprNode_traversFalseEnsuresConstraints
1795 (exprData_getSingle (data) ) );
1796 break;
1797
1798 case XPR_CALL:
4ab867d6 1799 ret = constraintList_addListFree (ret,
9280addf 1800 exprNode_traversFalseEnsuresConstraints
1801 (exprData_getFcn (data) ) );
1802 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1803 break;
1804
1805 case XPR_RETURN:
4ab867d6 1806 ret = constraintList_addListFree (ret,
9280addf 1807 exprNode_traversFalseEnsuresConstraints
1808 (exprData_getSingle (data) ) );
1809 break;
1810
1811 case XPR_NULLRETURN:
1812 // cstring_makeLiteral ("return");;
1813 break;
1814
1815 case XPR_FACCESS:
4ab867d6 1816 ret = constraintList_addListFree (ret,
9280addf 1817 exprNode_traversFalseEnsuresConstraints
1818 (exprData_getFieldNode (data) ) );
1819 //exprData_getFieldName (data) ;
1820 break;
1821
1822 case XPR_ARROW:
4ab867d6 1823 ret = constraintList_addListFree (ret,
9280addf 1824 exprNode_traversFalseEnsuresConstraints
1825 (exprData_getFieldNode (data) ) );
1826 // exprData_getFieldName (data);
1827 break;
1828
1829 case XPR_STRINGLITERAL:
1830 // cstring_copy (exprData_getLiteral (data));
1831 break;
1832
1833 case XPR_NUMLIT:
1834 // cstring_copy (exprData_getLiteral (data));
1835 break;
1836 case XPR_POSTOP:
1837
4ab867d6 1838 ret = constraintList_addListFree (ret,
9280addf 1839 exprNode_traversFalseEnsuresConstraints
1840 (exprData_getUopNode (data) ) );
1841 break;
470b7798 1842
1843 case XPR_CAST:
1844
4ab867d6 1845 ret = constraintList_addListFree (ret,
470b7798 1846 exprNode_traversFalseEnsuresConstraints
1847 (exprData_getCastNode (data) ) );
1848 break;
1849
9280addf 1850 default:
1851 break;
1852 }
1853
1854 return ret;
1855}
1856
616915dd 1857
1858/* walk down the tree and get all requires Constraints in each subexpression*/
d46ce6a4 1859/*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e)
616915dd 1860{
470b7798 1861 exprNode t1;
616915dd 1862
1863 bool handledExprNode;
1864 // char * mes;
1865 exprData data;
1866 constraintList ret;
1867
1868 if (exprNode_handleError (e))
1869 {
c3e695ff 1870 ret = constraintList_makeNew();
616915dd 1871 return ret;
1872 }
1873 ret = constraintList_copy (e->requiresConstraints );
1874
1875 handledExprNode = TRUE;
1876
1877 data = e->edata;
1878
1879 switch (e->kind)
1880 {
9280addf 1881 case XPR_WHILEPRED:
1882 t1 = exprData_getSingle (data);
4ab867d6 1883 ret = constraintList_addListFree ( ret, exprNode_traversRequiresConstraints (t1) );
9280addf 1884 break;
616915dd 1885
1886 case XPR_FETCH:
1887
4ab867d6 1888 ret = constraintList_addListFree (ret,
616915dd 1889 exprNode_traversRequiresConstraints
1890 (exprData_getPairA (data) ) );
1891
4ab867d6 1892 ret = constraintList_addListFree (ret,
616915dd 1893 exprNode_traversRequiresConstraints
1894 (exprData_getPairB (data) ) );
1895 break;
1896 case XPR_PREOP:
1897
4ab867d6 1898 ret = constraintList_addListFree (ret,
616915dd 1899 exprNode_traversRequiresConstraints
1900 (exprData_getUopNode (data) ) );
1901 break;
1902
1903 case XPR_PARENS:
4ab867d6 1904 ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
616915dd 1905 (exprData_getUopNode (data) ) );
1906 break;
2681ee39 1907 case XPR_INIT:
1908 ret = constraintList_addListFree (ret,
1909 exprNode_traversRequiresConstraints
1910 (exprData_getInitNode (data) ) );
1911 break;
1912
616915dd 1913 case XPR_ASSIGN:
4ab867d6 1914 ret = constraintList_addListFree (ret,
616915dd 1915 exprNode_traversRequiresConstraints
1916 (exprData_getOpA (data) ) );
1917
4ab867d6 1918 ret = constraintList_addListFree (ret,
616915dd 1919 exprNode_traversRequiresConstraints
1920 (exprData_getOpB (data) ) );
1921 break;
1922 case XPR_OP:
4ab867d6 1923 ret = constraintList_addListFree (ret,
616915dd 1924 exprNode_traversRequiresConstraints
1925 (exprData_getOpA (data) ) );
1926
4ab867d6 1927 ret = constraintList_addListFree (ret,
616915dd 1928 exprNode_traversRequiresConstraints
1929 (exprData_getOpB (data) ) );
1930 break;
1931 case XPR_SIZEOFT:
1932
1933 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1934
1935 break;
1936
1937 case XPR_SIZEOF:
1938
4ab867d6 1939 ret = constraintList_addListFree (ret,
616915dd 1940 exprNode_traversRequiresConstraints
1941 (exprData_getSingle (data) ) );
1942 break;
1943
1944 case XPR_CALL:
4ab867d6 1945 ret = constraintList_addListFree (ret,
616915dd 1946 exprNode_traversRequiresConstraints
1947 (exprData_getFcn (data) ) );
1948 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1949 break;
1950
1951 case XPR_RETURN:
4ab867d6 1952 ret = constraintList_addListFree (ret,
616915dd 1953 exprNode_traversRequiresConstraints
1954 (exprData_getSingle (data) ) );
1955 break;
1956
1957 case XPR_NULLRETURN:
1958 // cstring_makeLiteral ("return");;
1959 break;
1960
1961 case XPR_FACCESS:
4ab867d6 1962 ret = constraintList_addListFree (ret,
616915dd 1963 exprNode_traversRequiresConstraints
1964 (exprData_getFieldNode (data) ) );
1965 //exprData_getFieldName (data) ;
1966 break;
1967
1968 case XPR_ARROW:
4ab867d6 1969 ret = constraintList_addListFree (ret,
616915dd 1970 exprNode_traversRequiresConstraints
1971 (exprData_getFieldNode (data) ) );
1972 // exprData_getFieldName (data);
1973 break;
1974
1975 case XPR_STRINGLITERAL:
1976 // cstring_copy (exprData_getLiteral (data));
1977 break;
1978
1979 case XPR_NUMLIT:
1980 // cstring_copy (exprData_getLiteral (data));
1981 break;
1982 case XPR_POSTOP:
1983
4ab867d6 1984 ret = constraintList_addListFree (ret,
616915dd 1985 exprNode_traversRequiresConstraints
1986 (exprData_getUopNode (data) ) );
1987 break;
470b7798 1988
1989 case XPR_CAST:
1990
4ab867d6 1991 ret = constraintList_addListFree (ret,
470b7798 1992 exprNode_traversRequiresConstraints
1993 (exprData_getCastNode (data) ) );
1994 break;
1995
616915dd 1996 default:
1997 break;
1998 }
1999
2000 return ret;
2001}
2002
2003
2004/* walk down the tree and get all Ensures Constraints in each subexpression*/
d46ce6a4 2005/*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e)
616915dd 2006{
470b7798 2007 exprNode t1;
616915dd 2008
2009 bool handledExprNode;
2010 // char * mes;
2011 exprData data;
2012 // constraintExpr tmp;
2013 // constraint cons;
2014 constraintList ret;
2015
2016
2017 if (exprNode_handleError (e))
2018 {
c3e695ff 2019 ret = constraintList_makeNew();
616915dd 2020 return ret;
2021 }
2022
2023 ret = constraintList_copy (e->ensuresConstraints );
2024 handledExprNode = TRUE;
2025
2026 data = e->edata;
2027
2028 DPRINTF( (message (
2029 "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
2030 exprNode_unparse (e),
2031 constraintList_print(e->ensuresConstraints)
2032 )
2033 ));
2034
2035
2036 switch (e->kind)
2037 {
9280addf 2038 case XPR_WHILEPRED:
2039 t1 = exprData_getSingle (data);
4ab867d6 2040 ret = constraintList_addListFree ( ret,exprNode_traversEnsuresConstraints (t1) );
9280addf 2041 break;
616915dd 2042
2043 case XPR_FETCH:
2044
4ab867d6 2045 ret = constraintList_addListFree (ret,
616915dd 2046 exprNode_traversEnsuresConstraints
2047 (exprData_getPairA (data) ) );
2048
4ab867d6 2049 ret = constraintList_addListFree (ret,
616915dd 2050 exprNode_traversEnsuresConstraints
2051 (exprData_getPairB (data) ) );
2052 break;
2053 case XPR_PREOP:
2054
4ab867d6 2055 ret = constraintList_addListFree (ret,
616915dd 2056 exprNode_traversEnsuresConstraints
2057 (exprData_getUopNode (data) ) );
2058 break;
2059
2060 case XPR_PARENS:
4ab867d6 2061 ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
616915dd 2062 (exprData_getUopNode (data) ) );
2063 break;
2681ee39 2064
2065 case XPR_INIT:
2066 ret = constraintList_addListFree (ret,
2067 exprNode_traversEnsuresConstraints
2068 (exprData_getInitNode (data) ) );
2069 break;
2070
2071
616915dd 2072 case XPR_ASSIGN:
4ab867d6 2073 ret = constraintList_addListFree (ret,
616915dd 2074 exprNode_traversEnsuresConstraints
2075 (exprData_getOpA (data) ) );
2076
4ab867d6 2077 ret = constraintList_addListFree (ret,
616915dd 2078 exprNode_traversEnsuresConstraints
2079 (exprData_getOpB (data) ) );
2080 break;
2081 case XPR_OP:
4ab867d6 2082 ret = constraintList_addListFree (ret,
616915dd 2083 exprNode_traversEnsuresConstraints
2084 (exprData_getOpA (data) ) );
2085
4ab867d6 2086 ret = constraintList_addListFree (ret,
616915dd 2087 exprNode_traversEnsuresConstraints
2088 (exprData_getOpB (data) ) );
2089 break;
2090 case XPR_SIZEOFT:
2091
2092 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
2093
2094 break;
2095
2096 case XPR_SIZEOF:
2097
4ab867d6 2098 ret = constraintList_addListFree (ret,
616915dd 2099 exprNode_traversEnsuresConstraints
2100 (exprData_getSingle (data) ) );
2101 break;
2102
2103 case XPR_CALL:
4ab867d6 2104 ret = constraintList_addListFree (ret,
616915dd 2105 exprNode_traversEnsuresConstraints
2106 (exprData_getFcn (data) ) );
2107 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
2108 break;
2109
2110 case XPR_RETURN:
4ab867d6 2111 ret = constraintList_addListFree (ret,
616915dd 2112 exprNode_traversEnsuresConstraints
2113 (exprData_getSingle (data) ) );
2114 break;
2115
2116 case XPR_NULLRETURN:
2117 // cstring_makeLiteral ("return");;
2118 break;
2119
2120 case XPR_FACCESS:
4ab867d6 2121 ret = constraintList_addListFree (ret,
616915dd 2122 exprNode_traversEnsuresConstraints
2123 (exprData_getFieldNode (data) ) );
2124 //exprData_getFieldName (data) ;
2125 break;
2126
2127 case XPR_ARROW:
4ab867d6 2128 ret = constraintList_addListFree (ret,
616915dd 2129 exprNode_traversEnsuresConstraints
2130 (exprData_getFieldNode (data) ) );
2131 // exprData_getFieldName (data);
2132 break;
2133
2134 case XPR_STRINGLITERAL:
2135 // cstring_copy (exprData_getLiteral (data));
2136 break;
2137
2138 case XPR_NUMLIT:
2139 // cstring_copy (exprData_getLiteral (data));
2140 break;
2141 case XPR_POSTOP:
2142
4ab867d6 2143 ret = constraintList_addListFree (ret,
616915dd 2144 exprNode_traversEnsuresConstraints
2145 (exprData_getUopNode (data) ) );
2146 break;
470b7798 2147 case XPR_CAST:
2148
4ab867d6 2149 ret = constraintList_addListFree (ret,
470b7798 2150 exprNode_traversEnsuresConstraints
2151 (exprData_getCastNode (data) ) );
2152 break;
2153
616915dd 2154 default:
2155 break;
2156 }
2157DPRINTF( (message (
2158 "exprnode_traversEnsuresConstraints call for %s with constraintList of is returning %s",
2159 exprNode_unparse (e),
2160 // constraintList_print(e->ensuresConstraints),
2161 constraintList_print(ret)
2162 )
2163 ));
2164
2165
2166 return ret;
2167}
2168
28bf4b0b 2169/*drl moved out of constraintResolve.c 07-02-001 */
2170void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, fileloc sequencePoint)
2171{
2172 temp->requiresConstraints = constraintList_makeNew();
2173 temp->ensuresConstraints = constraintList_makeNew();
2174 temp->trueEnsuresConstraints = constraintList_makeNew();
2175 temp->falseEnsuresConstraints = constraintList_makeNew();
2176
2177 exprNodeList_elements (arglist, el)
2178 {
2179 constraintList temp2;
2180 exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
2181 temp2 = el->requiresConstraints;
2182 el->requiresConstraints = exprNode_traversRequiresConstraints(el);
2183 constraintList_free(temp2);
2184
2185 temp2 = el->ensuresConstraints;
2186 el->ensuresConstraints = exprNode_traversEnsuresConstraints(el);
2187 constraintList_free(temp2);
2188
2189 temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
2190 el->requiresConstraints);
2191
2192 temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
2193 el->ensuresConstraints);
2194 }
2195 end_exprNodeList_elements;
2196
2197}
2198
2199/*drl moved out of constraintResolve.c 07-03-001 */
2200constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
2201{
2202 constraintList postconditions;
2203 uentry temp;
2204 DPRINTF( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) );
2205
2206 temp = exprNode_getUentry (fcn);
2207
2208 postconditions = uentry_getFcnPostconditions (temp);
2209
2210 if (constraintList_isDefined(postconditions) )
2211 {
2212 postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
2213 postconditions = constraintList_doFixResult (postconditions, fcnCall);
2214 }
2215 else
2216 {
2217 postconditions = constraintList_makeNew();
2218 }
2219
2220 return postconditions;
2221}
2222
2223
2224/*drl moved out of constraintResolve.c 07-02-001 */
2225constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
2226{
2227 constraintList preconditions;
2228 uentry temp;
2229 DPRINTF( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) );
2230
2231 temp = exprNode_getUentry (fcn);
2232
2233 preconditions = uentry_getFcnPreconditions (temp);
2234
2235 if (constraintList_isDefined(preconditions) )
2236 {
2237 preconditions = constraintList_togglePost (preconditions);
2238 preconditions = constraintList_preserveCallInfo(preconditions, fcn);
2239 preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
2240 }
2241 else
2242 {
2243 if (constraintList_isUndefined(preconditions) )
2244 preconditions = constraintList_makeNew();
2245 }
2246 DPRINTF (( message("Done checkCall\n") ));
2247 DPRINTF (( message("Returning list %q ", constraintList_printDetailed(preconditions) ) ));
2248 return preconditions;
2249}
git-cvsimport mirror of splint
This page took 0.394502 seconds and 5 git commands to generate.