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