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