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