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