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