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