]> 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 tracker issue 1837229.
[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_isPlus_Op (tok))
1432 {
1433 break;
1434 }
1435 else if (lltok_isExcl_Op (tok))
1436 {
1437 break;
1438 }
1439 else if (lltok_isTilde_Op (tok))
1440 {
1441 break;
1442 }
1443 else
1444 {
1445 llcontbug (message("Unsupported preop in %s", exprNode_unparse(e)));
1446 BADEXIT;
1447 }
1448 break;
1449
1450 case XPR_POSTOP:
1451 exprNode_exprTraverse (exprData_getUopNode (data), TRUE,
1452 definaterv, sequencePoint);
1453
1454 if (lltok_isIncOp (exprData_getUopTok (data)))
1455 {
1456 DPRINTF(("doing ++"));
1457 t1 = exprData_getUopNode (data);
1458 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint);
1459 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1460 }
1461 if (lltok_isDecOp (exprData_getUopTok (data)))
1462 {
1463 DPRINTF(("doing --"));
1464 t1 = exprData_getUopNode (data);
1465 cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint);
1466 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1467 }
1468 break;
1469 case XPR_CAST:
1470 {
1471 t2 = exprData_getCastNode (data);
1472 DPRINTF ((message ("Examining cast (%q)%s",
1473 qtype_unparse (exprData_getCastType (data)),
1474 exprNode_unparse (t2))
1475 ));
1476 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1477 }
1478 break;
1479
1480 case XPR_COND:
1481 {
1482 exprNode pred, trueBranch, falseBranch;
1483 llassert(FALSE);
1484 pred = exprData_getTriplePred (data);
1485 trueBranch = exprData_getTripleTrue (data);
1486 falseBranch = exprData_getTripleFalse (data);
1487
1488 llassert (exprNode_isDefined (pred));
1489 llassert (exprNode_isDefined (trueBranch));
1490 llassert (exprNode_isDefined (falseBranch));
1491
1492 exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint);
1493
1494 temp = pred->ensuresConstraints;
1495 pred->ensuresConstraints = exprNode_traverseEnsuresConstraints(pred);
1496 constraintList_free(temp);
1497
1498 temp = pred->requiresConstraints;
1499 pred->requiresConstraints = exprNode_traverseRequiresConstraints(pred);
1500 constraintList_free(temp);
1501
1502 temp = pred->trueEnsuresConstraints;
1503 pred->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(pred);
1504 constraintList_free(temp);
1505
1506 temp = pred->falseEnsuresConstraints;
1507 pred->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(pred);
1508 constraintList_free(temp);
1509
1510 exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint);
1511
1512 temp = trueBranch->ensuresConstraints;
1513 trueBranch->ensuresConstraints = exprNode_traverseEnsuresConstraints(trueBranch);
1514 constraintList_free(temp);
1515
1516 temp = trueBranch->requiresConstraints;
1517 trueBranch->requiresConstraints = exprNode_traverseRequiresConstraints(trueBranch);
1518 constraintList_free(temp);
1519
1520 temp = trueBranch->trueEnsuresConstraints;
1521 trueBranch->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(trueBranch);
1522 constraintList_free(temp);
1523
1524 temp = trueBranch->falseEnsuresConstraints;
1525 trueBranch->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(trueBranch);
1526 constraintList_free(temp);
1527
1528 exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint);
1529
1530 temp = falseBranch->ensuresConstraints;
1531 falseBranch->ensuresConstraints = exprNode_traverseEnsuresConstraints(falseBranch);
1532 constraintList_free(temp);
1533
1534
1535 temp = falseBranch->requiresConstraints;
1536 falseBranch->requiresConstraints = exprNode_traverseRequiresConstraints(falseBranch);
1537 constraintList_free(temp);
1538
1539 temp = falseBranch->trueEnsuresConstraints;
1540 falseBranch->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(falseBranch);
1541 constraintList_free(temp);
1542
1543 temp = falseBranch->falseEnsuresConstraints;
1544 falseBranch->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(falseBranch);
1545 constraintList_free(temp);
1546
1547 /* if pred is true e equals true otherwise pred equals false */
1548
1549 cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1550 trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
1551
1552 cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1553 falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
1554
1555 e = doIfElse (e, pred, trueBranch, falseBranch);
1556 }
1557 break;
1558 case XPR_COMMA:
1559 llassert(FALSE);
1560 t1 = exprData_getPairA (data);
1561 t2 = exprData_getPairB (data);
1562 /* we essiantially treat this like expr1; expr2
1563 of course sequencePoint isn't adjusted so this isn't completely accurate
1564 problems...
1565 */
1566 exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint);
1567 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1568 exprNode_mergeResolve (e, t1, t2);
1569 break;
1570
1571 default:
1572 break;
1573 }
1574
1575 e->requiresConstraints = constraintList_preserveOrig (e->requiresConstraints);
1576 e->ensuresConstraints = constraintList_preserveOrig (e->ensuresConstraints);
1577 e->requiresConstraints = constraintList_addGeneratingExpr (e->requiresConstraints, e);
1578 e->ensuresConstraints = constraintList_addGeneratingExpr (e->ensuresConstraints, e);
1579 e->requiresConstraints = constraintList_removeSurpressed (e->requiresConstraints);
1580
1581 DPRINTF (("ensures constraints for %s are %s",
1582 exprNode_unparse(e), constraintList_unparseDetailed (e->ensuresConstraints)));
1583
1584 DPRINTF (("Requires constraints for %s are %s", exprNode_unparse(e),
1585 constraintList_unparseDetailed(e->ensuresConstraints)));
1586
1587 DPRINTF (("trueEnsures constraints for %s are %s", exprNode_unparse(e),
1588 constraintList_unparseDetailed(e->trueEnsuresConstraints)));
1589
1590 DPRINTF (("falseEnsures constraints for %s are %s", exprNode_unparse(e),
1591 constraintList_unparseDetailed(e->falseEnsuresConstraints)));
1592 return;
1593}
1594
1595
1596constraintList exprNode_traverseTrueEnsuresConstraints (exprNode e)
1597{
1598 exprNode t1;
1599
1600 bool handledExprNode;
1601 exprData data;
1602 constraintList ret;
1603
1604 if (exprNode_handleError (e))
1605 {
1606 ret = constraintList_makeNew();
1607 return ret;
1608 }
1609
1610 ret = constraintList_copy (e->trueEnsuresConstraints);
1611
1612 handledExprNode = TRUE;
1613
1614 data = e->edata;
1615
1616 switch (e->kind)
1617 {
1618 case XPR_WHILEPRED:
1619 t1 = exprData_getSingle (data);
1620 ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (t1));
1621 break;
1622
1623 case XPR_FETCH:
1624
1625 ret = constraintList_addListFree (ret,
1626 exprNode_traverseTrueEnsuresConstraints
1627 (exprData_getPairA (data)));
1628
1629 ret = constraintList_addListFree (ret,
1630 exprNode_traverseTrueEnsuresConstraints
1631 (exprData_getPairB (data)));
1632 break;
1633 case XPR_PREOP:
1634
1635 ret = constraintList_addListFree (ret,
1636 exprNode_traverseTrueEnsuresConstraints
1637 (exprData_getUopNode (data)));
1638 break;
1639
1640 case XPR_PARENS:
1641 ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints
1642 (exprData_getUopNode (data)));
1643 break;
1644
1645 case XPR_INIT:
1646 ret = constraintList_addListFree (ret,
1647 exprNode_traverseTrueEnsuresConstraints
1648 (exprData_getInitNode (data)));
1649 break;
1650
1651
1652 case XPR_ASSIGN:
1653 ret = constraintList_addListFree (ret,
1654 exprNode_traverseTrueEnsuresConstraints
1655 (exprData_getOpA (data)));
1656
1657 ret = constraintList_addListFree (ret,
1658 exprNode_traverseTrueEnsuresConstraints
1659 (exprData_getOpB (data)));
1660 break;
1661 case XPR_OP:
1662 ret = constraintList_addListFree (ret,
1663 exprNode_traverseTrueEnsuresConstraints
1664 (exprData_getOpA (data)));
1665
1666 ret = constraintList_addListFree (ret,
1667 exprNode_traverseTrueEnsuresConstraints
1668 (exprData_getOpB (data)));
1669 break;
1670 case XPR_SIZEOFT:
1671 break;
1672
1673 case XPR_SIZEOF:
1674
1675 ret = constraintList_addListFree (ret,
1676 exprNode_traverseTrueEnsuresConstraints
1677 (exprData_getSingle (data)));
1678 break;
1679
1680 case XPR_CALL:
1681 ret = constraintList_addListFree (ret,
1682 exprNode_traverseTrueEnsuresConstraints
1683 (exprData_getFcn (data)));
1684 break;
1685
1686 case XPR_RETURN:
1687 ret = constraintList_addListFree (ret,
1688 exprNode_traverseTrueEnsuresConstraints
1689 (exprData_getSingle (data)));
1690 break;
1691
1692 case XPR_NULLRETURN:
1693 break;
1694
1695 case XPR_FACCESS:
1696 ret = constraintList_addListFree (ret,
1697 exprNode_traverseTrueEnsuresConstraints
1698 (exprData_getFieldNode (data)));
1699 break;
1700
1701 case XPR_ARROW:
1702 ret = constraintList_addListFree (ret,
1703 exprNode_traverseTrueEnsuresConstraints
1704 (exprData_getFieldNode (data)));
1705 break;
1706
1707 case XPR_STRINGLITERAL:
1708 break;
1709
1710 case XPR_NUMLIT:
1711 break;
1712 case XPR_POSTOP:
1713
1714 ret = constraintList_addListFree (ret,
1715 exprNode_traverseTrueEnsuresConstraints
1716 (exprData_getUopNode (data)));
1717 break;
1718
1719 case XPR_CAST:
1720
1721 ret = constraintList_addListFree (ret,
1722 exprNode_traverseTrueEnsuresConstraints
1723 (exprData_getCastNode (data)));
1724 break;
1725
1726 default:
1727 break;
1728 }
1729
1730 return ret;
1731}
1732
1733constraintList exprNode_traverseFalseEnsuresConstraints (exprNode e)
1734{
1735 exprNode t1;
1736 bool handledExprNode;
1737 exprData data;
1738 constraintList ret;
1739
1740 if (exprNode_handleError (e))
1741 {
1742 ret = constraintList_makeNew();
1743 return ret;
1744 }
1745
1746 ret = constraintList_copy (e->falseEnsuresConstraints);
1747 handledExprNode = TRUE;
1748 data = e->edata;
1749
1750 switch (e->kind)
1751 {
1752 case XPR_WHILEPRED:
1753 t1 = exprData_getSingle (data);
1754 ret = constraintList_addListFree (ret,exprNode_traverseFalseEnsuresConstraints (t1));
1755 break;
1756
1757 case XPR_FETCH:
1758
1759 ret = constraintList_addListFree (ret,
1760 exprNode_traverseFalseEnsuresConstraints
1761 (exprData_getPairA (data)));
1762
1763 ret = constraintList_addListFree (ret,
1764 exprNode_traverseFalseEnsuresConstraints
1765 (exprData_getPairB (data)));
1766 break;
1767 case XPR_PREOP:
1768
1769 ret = constraintList_addListFree (ret,
1770 exprNode_traverseFalseEnsuresConstraints
1771 (exprData_getUopNode (data)));
1772 break;
1773
1774 case XPR_PARENS:
1775 ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints
1776 (exprData_getUopNode (data)));
1777 break;
1778 case XPR_INIT:
1779 ret = constraintList_addListFree (ret,
1780 exprNode_traverseFalseEnsuresConstraints
1781 ( exprData_getInitNode (data)));
1782 break;
1783
1784 case XPR_ASSIGN:
1785 ret = constraintList_addListFree (ret,
1786 exprNode_traverseFalseEnsuresConstraints
1787 (exprData_getOpA (data)));
1788
1789 ret = constraintList_addListFree (ret,
1790 exprNode_traverseFalseEnsuresConstraints
1791 (exprData_getOpB (data)));
1792 break;
1793 case XPR_OP:
1794 ret = constraintList_addListFree (ret,
1795 exprNode_traverseFalseEnsuresConstraints
1796 (exprData_getOpA (data)));
1797
1798 ret = constraintList_addListFree (ret,
1799 exprNode_traverseFalseEnsuresConstraints
1800 (exprData_getOpB (data)));
1801 break;
1802 case XPR_SIZEOFT:
1803 break;
1804
1805 case XPR_SIZEOF:
1806
1807 ret = constraintList_addListFree (ret,
1808 exprNode_traverseFalseEnsuresConstraints
1809 (exprData_getSingle (data)));
1810 break;
1811
1812 case XPR_CALL:
1813 ret = constraintList_addListFree (ret,
1814 exprNode_traverseFalseEnsuresConstraints
1815 (exprData_getFcn (data)));
1816 break;
1817
1818 case XPR_RETURN:
1819 ret = constraintList_addListFree (ret,
1820 exprNode_traverseFalseEnsuresConstraints
1821 (exprData_getSingle (data)));
1822 break;
1823
1824 case XPR_NULLRETURN:
1825 break;
1826
1827 case XPR_FACCESS:
1828 ret = constraintList_addListFree (ret,
1829 exprNode_traverseFalseEnsuresConstraints
1830 (exprData_getFieldNode (data)));
1831 break;
1832
1833 case XPR_ARROW:
1834 ret = constraintList_addListFree (ret,
1835 exprNode_traverseFalseEnsuresConstraints
1836 (exprData_getFieldNode (data)));
1837 break;
1838
1839 case XPR_STRINGLITERAL:
1840 break;
1841
1842 case XPR_NUMLIT:
1843 break;
1844 case XPR_POSTOP:
1845
1846 ret = constraintList_addListFree (ret,
1847 exprNode_traverseFalseEnsuresConstraints
1848 (exprData_getUopNode (data)));
1849 break;
1850
1851 case XPR_CAST:
1852
1853 ret = constraintList_addListFree (ret,
1854 exprNode_traverseFalseEnsuresConstraints
1855 (exprData_getCastNode (data)));
1856 break;
1857
1858 default:
1859 break;
1860 }
1861
1862 return ret;
1863}
1864
1865
1866/* walk down the tree and get all requires Constraints in each subexpression*/
1867/*@only@*/ constraintList exprNode_traverseRequiresConstraints (exprNode e)
1868{
1869 exprNode t1;
1870
1871 bool handledExprNode;
1872 exprData data;
1873 constraintList ret;
1874
1875 if (exprNode_handleError (e))
1876 {
1877 ret = constraintList_makeNew();
1878 return ret;
1879 }
1880
1881 ret = constraintList_copy (e->requiresConstraints);
1882 handledExprNode = TRUE;
1883 data = e->edata;
1884
1885 switch (e->kind)
1886 {
1887 case XPR_WHILEPRED:
1888 t1 = exprData_getSingle (data);
1889 ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (t1));
1890 break;
1891
1892 case XPR_FETCH:
1893
1894 ret = constraintList_addListFree (ret,
1895 exprNode_traverseRequiresConstraints
1896 (exprData_getPairA (data)));
1897
1898 ret = constraintList_addListFree (ret,
1899 exprNode_traverseRequiresConstraints
1900 (exprData_getPairB (data)));
1901 break;
1902 case XPR_PREOP:
1903
1904 ret = constraintList_addListFree (ret,
1905 exprNode_traverseRequiresConstraints
1906 (exprData_getUopNode (data)));
1907 break;
1908
1909 case XPR_PARENS:
1910 ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints
1911 (exprData_getUopNode (data)));
1912 break;
1913 case XPR_INIT:
1914 ret = constraintList_addListFree (ret,
1915 exprNode_traverseRequiresConstraints
1916 (exprData_getInitNode (data)));
1917 break;
1918
1919 case XPR_ASSIGN:
1920 ret = constraintList_addListFree (ret,
1921 exprNode_traverseRequiresConstraints
1922 (exprData_getOpA (data)));
1923
1924 ret = constraintList_addListFree (ret,
1925 exprNode_traverseRequiresConstraints
1926 (exprData_getOpB (data)));
1927 break;
1928 case XPR_OP:
1929 ret = constraintList_addListFree (ret,
1930 exprNode_traverseRequiresConstraints
1931 (exprData_getOpA (data)));
1932
1933 ret = constraintList_addListFree (ret,
1934 exprNode_traverseRequiresConstraints
1935 (exprData_getOpB (data)));
1936 break;
1937 case XPR_SIZEOFT:
1938 break;
1939
1940 case XPR_SIZEOF:
1941
1942 ret = constraintList_addListFree (ret,
1943 exprNode_traverseRequiresConstraints
1944 (exprData_getSingle (data)));
1945 break;
1946
1947 case XPR_CALL:
1948 ret = constraintList_addListFree (ret,
1949 exprNode_traverseRequiresConstraints
1950 (exprData_getFcn (data)));
1951 break;
1952
1953 case XPR_RETURN:
1954 ret = constraintList_addListFree (ret,
1955 exprNode_traverseRequiresConstraints
1956 (exprData_getSingle (data)));
1957 break;
1958
1959 case XPR_NULLRETURN:
1960 break;
1961
1962 case XPR_FACCESS:
1963 ret = constraintList_addListFree (ret,
1964 exprNode_traverseRequiresConstraints
1965 (exprData_getFieldNode (data)));
1966 break;
1967
1968 case XPR_ARROW:
1969 ret = constraintList_addListFree (ret,
1970 exprNode_traverseRequiresConstraints
1971 (exprData_getFieldNode (data)));
1972 break;
1973
1974 case XPR_STRINGLITERAL:
1975 break;
1976
1977 case XPR_NUMLIT:
1978 break;
1979 case XPR_POSTOP:
1980
1981 ret = constraintList_addListFree (ret,
1982 exprNode_traverseRequiresConstraints
1983 (exprData_getUopNode (data)));
1984 break;
1985
1986 case XPR_CAST:
1987
1988 ret = constraintList_addListFree (ret,
1989 exprNode_traverseRequiresConstraints
1990 (exprData_getCastNode (data)));
1991 break;
1992
1993 default:
1994 break;
1995 }
1996
1997 return ret;
1998}
1999
2000
2001/* walk down the tree and get all Ensures Constraints in each subexpression*/
2002/*@only@*/ constraintList exprNode_traverseEnsuresConstraints (exprNode e)
2003{
2004 exprNode t1;
2005
2006 bool handledExprNode;
2007 exprData data;
2008 constraintList ret;
2009
2010 if (exprNode_handleError (e))
2011 {
2012 ret = constraintList_makeNew();
2013 return ret;
2014 }
2015
2016 ret = constraintList_copy (e->ensuresConstraints);
2017 handledExprNode = TRUE;
2018
2019 data = e->edata;
2020
2021 DPRINTF ((message ("exprnode_traversEnsuresConstraints call for %s with "
2022 "constraintList of %s",
2023 exprNode_unparse (e),
2024 constraintList_unparse(e->ensuresConstraints)
2025 )
2026 ));
2027
2028
2029 switch (e->kind)
2030 {
2031 case XPR_WHILEPRED:
2032 t1 = exprData_getSingle (data);
2033 ret = constraintList_addListFree (ret,exprNode_traverseEnsuresConstraints (t1));
2034 break;
2035
2036 case XPR_FETCH:
2037 ret = constraintList_addListFree (ret,
2038 exprNode_traverseEnsuresConstraints
2039 (exprData_getPairA (data)));
2040
2041 ret = constraintList_addListFree (ret,
2042 exprNode_traverseEnsuresConstraints
2043 (exprData_getPairB (data)));
2044 break;
2045 case XPR_PREOP:
2046 ret = constraintList_addListFree (ret,
2047 exprNode_traverseEnsuresConstraints
2048 (exprData_getUopNode (data)));
2049 break;
2050
2051 case XPR_PARENS:
2052 ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints
2053 (exprData_getUopNode (data)));
2054 break;
2055
2056 case XPR_INIT:
2057 ret = constraintList_addListFree (ret,
2058 exprNode_traverseEnsuresConstraints
2059 (exprData_getInitNode (data)));
2060 break;
2061
2062
2063 case XPR_ASSIGN:
2064 ret = constraintList_addListFree (ret,
2065 exprNode_traverseEnsuresConstraints
2066 (exprData_getOpA (data)));
2067
2068 ret = constraintList_addListFree (ret,
2069 exprNode_traverseEnsuresConstraints
2070 (exprData_getOpB (data)));
2071 break;
2072 case XPR_OP:
2073 ret = constraintList_addListFree (ret,
2074 exprNode_traverseEnsuresConstraints
2075 (exprData_getOpA (data)));
2076
2077 ret = constraintList_addListFree (ret,
2078 exprNode_traverseEnsuresConstraints
2079 (exprData_getOpB (data)));
2080 break;
2081 case XPR_SIZEOFT:
2082 break;
2083
2084 case XPR_SIZEOF:
2085 ret = constraintList_addListFree (ret,
2086 exprNode_traverseEnsuresConstraints
2087 (exprData_getSingle (data)));
2088 break;
2089 case XPR_CALL:
2090 ret = constraintList_addListFree (ret,
2091 exprNode_traverseEnsuresConstraints
2092 (exprData_getFcn (data)));
2093 break;
2094 case XPR_RETURN:
2095 ret = constraintList_addListFree (ret,
2096 exprNode_traverseEnsuresConstraints
2097 (exprData_getSingle (data)));
2098 break;
2099 case XPR_NULLRETURN:
2100 break;
2101 case XPR_FACCESS:
2102 ret = constraintList_addListFree (ret,
2103 exprNode_traverseEnsuresConstraints
2104 (exprData_getFieldNode (data)));
2105 break;
2106 case XPR_ARROW:
2107 ret = constraintList_addListFree (ret,
2108 exprNode_traverseEnsuresConstraints
2109 (exprData_getFieldNode (data)));
2110 break;
2111 case XPR_STRINGLITERAL:
2112 break;
2113 case XPR_NUMLIT:
2114 break;
2115 case XPR_POSTOP:
2116 ret = constraintList_addListFree (ret,
2117 exprNode_traverseEnsuresConstraints
2118 (exprData_getUopNode (data)));
2119 break;
2120 case XPR_CAST:
2121 ret = constraintList_addListFree (ret,
2122 exprNode_traverseEnsuresConstraints
2123 (exprData_getCastNode (data)));
2124 break;
2125 default:
2126 break;
2127 }
2128
2129 DPRINTF((message ("exprnode_traversEnsuresConstraints call for %s with "
2130 "constraintList of is returning %s",
2131 exprNode_unparse (e),
2132 constraintList_unparse(ret))));
2133
2134 return ret;
2135}
2136
2137/*drl moved out of constraintResolve.c 07-02-001 */
2138void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist,
2139 fileloc sequencePoint)
2140{
2141
2142 llassert(temp != NULL );
2143
2144 temp->requiresConstraints = constraintList_makeNew();
2145 temp->ensuresConstraints = constraintList_makeNew();
2146 temp->trueEnsuresConstraints = constraintList_makeNew();
2147 temp->falseEnsuresConstraints = constraintList_makeNew();
2148
2149 exprNodeList_elements (arglist, el)
2150 {
2151 constraintList temp2;
2152
2153 llassert(exprNode_isDefined(el) );
2154
2155 exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
2156 temp2 = el->requiresConstraints;
2157 el->requiresConstraints = exprNode_traverseRequiresConstraints(el);
2158 constraintList_free(temp2);
2159
2160 temp2 = el->ensuresConstraints;
2161 el->ensuresConstraints = exprNode_traverseEnsuresConstraints(el);
2162 constraintList_free(temp2);
2163
2164 temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
2165 el->requiresConstraints);
2166
2167 temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
2168 el->ensuresConstraints);
2169 }
2170 end_exprNodeList_elements;
2171
2172}
2173
2174/*drl moved out of constraintResolve.c 07-03-001 */
2175constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
2176{
2177 constraintList postconditions;
2178 uentry temp;
2179 DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist))));
2180
2181 temp = exprNode_getUentry (fcn);
2182
2183 postconditions = uentry_getFcnPostconditions (temp);
2184
2185 if (constraintList_isDefined (postconditions))
2186 {
2187 postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
2188 postconditions = constraintList_doFixResult (postconditions, fcnCall);
2189 }
2190 else
2191 {
2192 postconditions = constraintList_makeNew();
2193 }
2194
2195 return postconditions;
2196}
2197
2198/*
2199comment this out for now
2200we'll include it in a production release when its stable...
2201
2202 void findStructs (exprNodeList arglist)
2203{
2204
2205 ctype ct, rt;
2206
2207 DPRINTF((
2208 message("doing findStructs: %s", exprNodeList_unparse(arglist))
2209 ));
2210
2211
2212 exprNodeList_elements(arglist, expr)
2213 {
2214 ct = exprNode_getType(expr);
2215
2216 rt = ctype_realType (ct);
2217
2218 if (ctype_isStruct (rt))
2219 DPRINTF((message("Found structure %s", exprNode_unparse(expr))
2220 ));
2221 if (hasInvariants(ct))
2222 {
2223 constraintList invars;
2224
2225 invars = getInvariants(ct);
2226
2227
2228 DPRINTF((message ("findStructs has invariants %s ", constraintList_unparse (invars))
2229 ));
2230
2231 invars = constraintList_doSRefFixStructConstraint(invars, exprNode_getSref(expr), ct);
2232
2233
2234 DPRINTF((message ("findStructs finded invariants to be %s ", constraintList_unparse (invars))
2235 ));
2236 }
2237 }
2238 end_exprNodeList_elements;
2239}
2240
2241*/
2242
2243/*drl moved out of constraintResolve.c 07-02-001 */
2244constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
2245{
2246 constraintList preconditions;
2247 uentry temp;
2248 DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist))));
2249
2250 temp = exprNode_getUentry (fcn);
2251
2252 preconditions = uentry_getFcnPreconditions (temp);
2253
2254 if (constraintList_isDefined(preconditions))
2255 {
2256 preconditions = constraintList_togglePost (preconditions);
2257 preconditions = constraintList_preserveCallInfo(preconditions, fcn);
2258 preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
2259 }
2260 else
2261 {
2262 if (constraintList_isUndefined(preconditions))
2263 preconditions = constraintList_makeNew();
2264 }
2265
2266 if (context_getFlag (FLG_IMPBOUNDSCONSTRAINTS))
2267 {
2268
2269 /*
2270 uentryList_elements (arglist, el)
2271 {
2272 sRef s;
2273 DPRINTF((message("setImplicitfcnConstraints doing: %s", uentry_unparse(el) ) ));
2274
2275 s = uentry_getSref(el);
2276 if (sRef_isReference (s) )
2277 {
2278 DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
2279 }
2280 else
2281 {
2282 DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
2283 }
2284 //drl 4/26/01
2285 //chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0
2286 c = constraint_makeSRefWriteSafeInt (s, 0);
2287
2288 implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
2289
2290 //drl 10/23/2002 added support for out
2291 if (!uentry_isOut(el) )
2292 {
2293 c = constraint_makeSRefReadSafeInt (s, 0);
2294 implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
2295 }
2296
2297
2298 }
2299 */
2300 }
2301
2302 DPRINTF ((message("Done checkCall\n")));
2303 DPRINTF ((message("Returning list %q ", constraintList_unparseDetailed(preconditions))));
2304
2305 /*
2306 drl we're going to comment this out for now
2307 we'll include it if we're sure it's working
2308
2309 findStructs(arglist);
2310 */
2311
2312 return preconditions;
2313}
2314
2315/*drl added this function 10.29.001
2316 takes an exprNode of the form const + const
2317 and sets the value
2318*/
2319/*drl
2320 I'm a bit nervous about modifying the exprNode
2321 but this is the easy way to do this
2322 If I have time I'd like to cause the exprNode to get created correctly in the first place */
2323void exprNode_findValue(exprNode e)
2324{
2325 exprData data;
2326
2327 exprNode t1, t2;
2328 lltok tok;
2329
2330 llassert(exprNode_isDefined(e) );
2331
2332 data = e->edata;
2333
2334 if (exprNode_hasValue(e))
2335 return;
2336
2337 if (e->kind == XPR_OP)
2338 {
2339 t1 = exprData_getOpA (data);
2340 t2 = exprData_getOpB (data);
2341 tok = exprData_getOpTok (data);
2342
2343 exprNode_findValue(t1);
2344 exprNode_findValue(t2);
2345
2346 if (!(exprNode_knownIntValue(t1) && (exprNode_knownIntValue(t2))))
2347 return;
2348
2349 if (lltok_isPlus_Op (tok))
2350 {
2351 long v1, v2;
2352
2353 v1 = exprNode_getLongValue(t1);
2354 v2 = exprNode_getLongValue(t2);
2355
2356 if (multiVal_isDefined(e->val))
2357 multiVal_free (e->val);
2358
2359 e->val = multiVal_makeInt (v1 + v2);
2360 }
2361
2362 if (lltok_isMinus_Op (tok))
2363 {
2364 long v1, v2;
2365
2366 v1 = exprNode_getLongValue(t1);
2367 v2 = exprNode_getLongValue(t2);
2368
2369 if (multiVal_isDefined(e->val))
2370 {
2371 multiVal_free (e->val);
2372 }
2373
2374 e->val = multiVal_makeInt (v1 - v2);
2375 }
2376
2377 /*drl I should really do * and / at some point */
2378
2379 }
2380
2381}
2382
git-cvsimport mirror of splint
This page took 0.064115 seconds and 5 git commands to generate.