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