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