]> andersk Git - splint.git/blame - src/constraintGeneration.c
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Simple modification to tests.
[splint.git] / src / constraintGeneration.c
CommitLineData
616915dd 1
2/*
3** constraintGeneration.c
4*/
5
6//#define DEBUGPRINT 1
7
8# include <ctype.h> /* for isdigit */
9# include "lclintMacros.nf"
10# include "basic.h"
11# include "cgrammar.h"
12# include "cgrammar_tokens.h"
13
14# include "exprChecks.h"
15# include "aliasChecks.h"
16# include "exprNodeSList.h"
17
18# include "exprData.i"
19# include "exprDataQuite.i"
20
470b7798 21extern void forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody);
22
616915dd 23bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e);
24static bool exprNode_handleError( exprNode p_e);
25
26//static cstring exprNode_findConstraints ( exprNode p_e);
27static bool exprNode_isMultiStatement(exprNode p_e);
28static bool exprNode_multiStatement (exprNode p_e);
29bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint);
30//static void exprNode_constraintPropagateUp (exprNode p_e);
31constraintList exprNode_traversRequiresConstraints (exprNode e);
32constraintList exprNode_traversEnsuresConstraints (exprNode e);
33
34constraintList exprNode_traversTrueEnsuresConstraints (exprNode e);
9280addf 35constraintList exprNode_traversFalseEnsuresConstraints (exprNode e);
616915dd 36
37extern constraintList reflectChanges (constraintList pre2, constraintList post1);
38
39void mergeResolve (exprNode parent, exprNode child1, exprNode child2);
40exprNode makeDataTypeConstraints (exprNode e);
41constraintList constraintList_makeFixedArrayConstraints (sRefSet s);
42constraintList checkCall (exprNode fcn, exprNodeList arglist);
43
9280addf 44void checkArgumentList (exprNode temp, exprNodeList arglist, fileloc sequencePoint);
45
616915dd 46//bool exprNode_testd()
47//{
48 /* if ( ( (exprNode_isError ) ) )
49 {
50 }
51 if ( ( (e_1 ) ) )
52 {
53 }
54 */
55//}
56
57bool exprNode_isUnhandled (exprNode e)
58{
59 llassert( exprNode_isDefined(e) );
60 switch (e->kind)
61 {
62 case XPR_INITBLOCK:
63 case XPR_EMPTY:
64 case XPR_LABEL:
65 case XPR_CONST:
66 case XPR_VAR:
67 case XPR_BODY:
68 case XPR_OFFSETOF:
69 case XPR_ALIGNOFT:
70 case XPR_ALIGNOF:
71 case XPR_VAARG:
72 case XPR_ITERCALL:
73 case XPR_ITER:
74 case XPR_CAST:
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_SWITCH:
84 case XPR_FTCASE:
85 case XPR_CASE:
86 // case XPR_INIT:
87 case XPR_NODE:
88 DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) );
89 return TRUE;
90 /*@notreached@*/
91 break;
92 default:
93 return FALSE;
94
95 }
96 /*not reached*/
97 return FALSE;
98}
99
100bool exprNode_handleError( exprNode e)
101{
102 if (exprNode_isError (e) || exprNode_isUnhandled(e) )
103 {
104 static /*@only@*/ cstring error = cstring_undefined;
105
106 if (!cstring_isDefined (error))
107 {
108 error = cstring_makeLiteral ("<error>");
109 }
110
111 /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/
112 }
113 return FALSE;
114}
115
116bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e)
117{
118 if (exprNode_isError (e) )
119 return FALSE;
120
9280addf 121 e->requiresConstraints = constraintList_new();
122 e->ensuresConstraints = constraintList_new();
123 e->trueEnsuresConstraints = constraintList_new();
124 e->falseEnsuresConstraints = constraintList_new();
125
616915dd 126 if (exprNode_isUnhandled (e) )
127 {
128 DPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) );
9280addf 129 return FALSE;
616915dd 130 }
131
132
133 // e = makeDataTypeConstraints (e);
134
135 DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e),
136 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
137
138 if (exprNode_isMultiStatement ( e) )
139 {
140 exprNode_multiStatement(e);
141 }
142 else
143 {
9280addf 144 fileloc loc;
145
146 loc = exprNode_getNextSequencePoint(e);
147 exprNode_exprTraverse(e, FALSE, FALSE, loc);
148
616915dd 149 // llassert(FALSE);
150 return FALSE;
151 }
152
153 {
154 constraintList c;
155
156 c = constraintList_makeFixedArrayConstraints (e->uses);
157 e->requiresConstraints = reflectChanges (e->requiresConstraints, c);
158
159 // e->ensuresConstraints = constraintList_mergeEnsures(c, e->ensuresConstraints);
160
161 }
162
163 /* printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) );
164 printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) ); */
165 return FALSE;
166}
167
168
169/* handles multiple statements */
170
171bool exprNode_isMultiStatement(exprNode e)
172{
173if (exprNode_handleError (e) != NULL)
174 return FALSE;
175
176 switch (e->kind)
177 {
178 case XPR_FOR:
179 case XPR_FORPRED:
180 case XPR_IF:
181 case XPR_IFELSE:
182 case XPR_WHILE:
183 case XPR_WHILEPRED:
184 case XPR_DOWHILE:
185 case XPR_BLOCK:
186 case XPR_STMT:
187 case XPR_STMTLIST:
188 return TRUE;
189 default:
190 return FALSE;
191 }
192
193}
194
195bool exprNode_stmt (exprNode e)
196{
197 exprNode snode;
198 fileloc loc;
199 bool notError;
9280addf 200 char * s;
201
616915dd 202 if (exprNode_isError(e) )
203 {
204 return FALSE;
205 }
206 e->requiresConstraints = constraintList_new();
207 e->ensuresConstraints = constraintList_new();
208 // e = makeDataTypeConstraints(e);
209
210
211 DPRINTF(( "STMT:") );
9280addf 212 s = exprNode_unparse(e);
213 // DPRINTF ( ( message("STMT: %s ") ) );
214
616915dd 215 if (e->kind == XPR_INIT)
216 {
217 DPRINTF (("Init") );
218 DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
219 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
220 notError = exprNode_exprTraverse (e, FALSE, FALSE, loc);
221 e->requiresConstraints = exprNode_traversRequiresConstraints(e);
222 e->ensuresConstraints = exprNode_traversEnsuresConstraints(e);
223 return notError;
224 }
225
226 if (e->kind != XPR_STMT)
227 {
228
229 DPRINTF (("Not Stmt") );
230 DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
231 if (exprNode_isMultiStatement (e) )
232 {
233 return exprNode_multiStatement (e );
234 }
235 BPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) );
236 return TRUE;
237 // llassert(FALSE);
238 }
239
240 DPRINTF (("Stmt") );
241 DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
242
243 snode = exprData_getUopNode (e->edata);
244
245 /* could be stmt involving multiple statements:
246 i.e. if, while for ect.
247 */
248
249 if (exprNode_isMultiStatement (snode))
250 {
470b7798 251 bool temp;
252
253 temp = exprNode_multiStatement (snode);
254 exprNode_copyConstraints (e, snode);
255 return temp;
616915dd 256 }
257
258 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
259 notError = exprNode_exprTraverse (snode, FALSE, FALSE, loc);
260 e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
261 // printf ("For: %s \n", exprNode_unparse (e) );
262 // printf ("%s\n", constraintList_print(e->requiresConstraints) );
263 e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode);
264 // printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
265 // llassert(notError);
266 return notError;
267
268}
269
270
271bool exprNode_stmtList (exprNode e)
272{
273 exprNode stmt1, stmt2;
274 if (exprNode_isError (e) )
275 {
276 return FALSE;
277 }
278
279 e->requiresConstraints = constraintList_new();
280 e->ensuresConstraints = constraintList_new();
281 // e = makeDataTypeConstraints(e);
282
283 /*Handle case of stmtList with only one statement:
284 The parse tree stores this as stmt instead of stmtList*/
285 if (e->kind != XPR_STMTLIST)
286 {
287 return exprNode_stmt(e);
288 }
289 llassert (e->kind == XPR_STMTLIST);
290 DPRINTF(( "STMTLIST:") );
291 DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
292 stmt1 = exprData_getPairA (e->edata);
293 stmt2 = exprData_getPairB (e->edata);
294
295
296 DPRINTF((" stmtlist ") );
297 DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
298
299 exprNode_stmt (stmt1);
300 DPRINTF(("\nstmt after stmtList call " ));
301
302 exprNode_stmt (stmt2);
303 mergeResolve (e, stmt1, stmt2 );
304
305 DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
306 constraintList_print(e->requiresConstraints),
307 constraintList_print(e->ensuresConstraints) ) ) );
308 return TRUE;
309}
310
616915dd 311exprNode doIf (exprNode e, exprNode test, exprNode body)
312{
313 DPRINTF ((message ("doIf: %s ", exprNode_unparse(e) ) ) );
470b7798 314
315 llassert(test);
316 llassert(e);
317 llassert(body);
616915dd 318
319 test->ensuresConstraints = exprNode_traversEnsuresConstraints (test);
470b7798 320 test->requiresConstraints = exprNode_traversRequiresConstraints (test);
321
616915dd 322 test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
323
324 e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints);
325 e->requiresConstraints = reflectChanges (e->requiresConstraints,
326 test->ensuresConstraints);
470b7798 327 e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints);
328
616915dd 329#warning bad
330 e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
470b7798 331 /*
332 if (!exprNode_mayEscape (body) )
333 e->ensuresConstraints = constraintList_mergeEnsures (e->ensuresConstraints,
334 test->falseEnsuresConstraints);
335 */
9280addf 336 DPRINTF ((message ("doIf: if requiers %s ", constraintList_print(e->requiresConstraints) ) ) );
337
616915dd 338 return e;
339}
340
470b7798 341/*drl added 3/4/2001
342 Also used for condition i.e. ?: operation
343
344 Precondition
345 This function assumes that p, trueBranch, falseBranch have have all been traversed
346 for constraints i.e. we assume that exprNode_traversEnsuresConstraints,
347 exprNode_traversRequiresConstraints, exprNode_traversTrueEnsuresConstraints,
348 exprNode_traversFalseEnsuresConstraints have all been run
349*/
350
351
352exprNode doIfElse (/*@returned@*/ exprNode e, exprNode p, exprNode trueBranch, exprNode falseBranch)
353{
354
355 constraintList c1, cons, t, f;
356
357 // do requires clauses
358 c1 = constraintList_copy (p->ensuresConstraints);
359
360 t = reflectChanges (trueBranch->requiresConstraints, p->trueEnsuresConstraints);
361 t = reflectChanges (t, p->ensuresConstraints);
362
363 // e->requiresConstraints = constraintList_copy (cons);
364
365 cons = reflectChanges (falseBranch->requiresConstraints, p->falseEnsuresConstraints);
366 cons = reflectChanges (cons, c1);
367
368 e->requiresConstraints = constraintList_mergeRequires (t, cons);
369 e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, p->requiresConstraints);
370
371 // do ensures clauses
372 // find the the ensures lists for each subbranch
373 t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
374 t = constraintList_mergeEnsures (p->ensuresConstraints, t);
375
376 f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
377 f = constraintList_mergeEnsures (p->ensuresConstraints, f);
378
379 // find ensures for whole if/else statement
380
381 e->ensuresConstraints = constraintList_logicalOr (t, f);
382
383 return e;
384}
9280addf 385
386exprNode doWhile (exprNode e, exprNode test, exprNode body)
387{
388 DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e) ) ) );
389 return doIf (e, test, body);
390}
391
616915dd 392constraintList constraintList_makeFixedArrayConstraints (sRefSet s)
393{
394 constraintList ret;
470b7798 395 constraint con;
616915dd 396 ret = constraintList_new();
397
398 sRefSet_elements (s, el)
399 {
400 // llassert (el);
401 if (sRef_isFixedArray(el) )
402 {
403 int s;
470b7798 404 DPRINTF( (message("%s is a fixed array",
405 sRef_unparse(el)) ) );
406 //if (el->kind == SK_DERIVED)
407 // break; //hack until I find the real problem
616915dd 408 s = sRef_getArraySize(el);
409 DPRINTF( (message("%s is a fixed array with size %d",
410 sRef_unparse(el), s) ) );
411 con = constraint_makeSRefSetBufferSize (el, (s - 1));
412 //con = constraint_makeSRefWriteSafeInt (el, (s - 1));
413 ret = constraintList_add(ret, con);
414 }
415 else
416 {
417 DPRINTF( (message("%s is not a fixed array",
418 sRef_unparse(el)) ) );
470b7798 419
420
421 if (sRef_isExternallyVisible (el) )
422 {
423 /*DPRINTF( (message("%s is externally visible",
424 sRef_unparse(el) ) ));
425 con = constraint_makeSRefWriteSafeInt(el, 0);
426 ret = constraintList_add(ret, con);
427
428 con = constraint_makeSRefReadSafeInt(el, 0);
429
430 ret = constraintList_add(ret, con);*/
431 }
616915dd 432 }
433 }
434 end_sRefSet_elements
435
470b7798 436 DPRINTF(( message("constraintList_makeFixedArrayConstraints returning %s",
437 constraintList_print(ret) ) ));
616915dd 438 return ret;
439}
440
441exprNode makeDataTypeConstraints (exprNode e)
442{
443 constraintList c;
444 DPRINTF(("makeDataTypeConstraints"));
445
446 c = constraintList_makeFixedArrayConstraints (e->uses);
447
448 e->ensuresConstraints = constraintList_addList (e->ensuresConstraints, c);
449
450 return e;
451}
452
453void doFor (exprNode e, exprNode forPred, exprNode forBody)
454{
455 exprNode init, test, inc;
456 //merge the constraints: modle as if statement
457 /* init
458 if (test)
459 for body
460 inc */
461 init = exprData_getTripleInit (forPred->edata);
462 test = exprData_getTripleTest (forPred->edata);
463 inc = exprData_getTripleInc (forPred->edata);
464
465 if ( ( (exprNode_isError (test) /*|| (exprNode_isError(init) )*/ ) || (exprNode_isError (inc) ) ) )
466 {
467 DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e) ) ) );
468 return;
469 }
470
471 forLoopHeuristics(e, forPred, forBody);
472
473 e->requiresConstraints = reflectChanges (forBody->requiresConstraints, test->ensuresConstraints);
474 e->requiresConstraints = reflectChanges (e->requiresConstraints, test->trueEnsuresConstraints);
475 e->requiresConstraints = reflectChanges (e->requiresConstraints, forPred->ensuresConstraints);
476
477 if (!forBody->canBreak)
478 {
479 e->ensuresConstraints = constraintList_addList(e->ensuresConstraints, forPred->ensuresConstraints);
480 e->ensuresConstraints = constraintList_addList(e->ensuresConstraints, test->falseEnsuresConstraints);
481 }
482 else
483 {
484 DPRINTF(("Can break") );
485 }
486
487}
488
470b7798 489exprNode doSwitch (/*@returned@*/ exprNode e)
490{
491 exprNode body;
492 exprData data;
493
494 data = e->edata;
495 llassert(FALSE);
496 //TPRINTF (( message ("doSwitch for: switch (%s) %s",
497 // exprNode_unparse (exprData_getPairA (data)),
498 // exprNode_unparse (exprData_getPairB (data))) ));
499
500 body = exprData_getPairB (data);
501
502 // exprNode_generateConstraints(body);
503
504 // e->requiresConstraints = constraintList_copy ( body->requiresConstraints );
505 //e->ensuresConstraints = constraintList_copy ( body->ensuresConstraints );
506
507 return e;
508}
9280addf 509
510
616915dd 511bool exprNode_multiStatement (exprNode e)
512{
513
514 bool ret;
515 exprData data;
516 exprNode e1, e2;
517 exprNode p, trueBranch, falseBranch;
518 exprNode forPred, forBody;
470b7798 519 exprNode test;
520 // constraintList t, f;
616915dd 521 e->requiresConstraints = constraintList_new();
522 e->ensuresConstraints = constraintList_new();
523 e->trueEnsuresConstraints = constraintList_new();
524 e->falseEnsuresConstraints = constraintList_new();
525
526 // e = makeDataTypeConstraints(e);
527
528 DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
529 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
530
531 if (exprNode_handleError (e))
532 {
533 return FALSE;
534 }
535
536 data = e->edata;
537
538 ret = TRUE;
539
540 switch (e->kind)
541 {
542
543 case XPR_FOR:
544 // ret = message ("%s %s",
545 forPred = exprData_getPairA (data);
546 forBody = exprData_getPairB (data);
547
548 //first generate the constraints
549 exprNode_generateConstraints (forPred);
550 exprNode_generateConstraints (forBody);
551
552
553 doFor (e, forPred, forBody);
554
555 break;
556
557 case XPR_FORPRED:
558 // ret = message ("for (%s; %s; %s)",
559 exprNode_generateConstraints (exprData_getTripleInit (data) );
560 test = exprData_getTripleTest (data);
561 exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
9280addf 562 exprNode_generateConstraints (exprData_getTripleInc (data) );
563
616915dd 564 if (!exprNode_isError(test) )
565 test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
566
567 exprNode_generateConstraints (exprData_getTripleInc (data));
568 break;
9280addf 569
570 case XPR_WHILE:
571 e1 = exprData_getPairA (data);
572 e2 = exprData_getPairB (data);
573
574 exprNode_exprTraverse (e1,
575 FALSE, FALSE, exprNode_loc(e1));
576
577 exprNode_generateConstraints (e2);
578
579 e = doWhile (e, e1, e2);
580
581 break;
582
616915dd 583 case XPR_IF:
584 DPRINTF(( "IF:") );
585 DPRINTF ((exprNode_unparse(e) ) );
586 // ret = message ("if (%s) %s",
587 e1 = exprData_getPairA (data);
588 e2 = exprData_getPairB (data);
589
590 exprNode_exprTraverse (e1,
591 FALSE, FALSE, exprNode_loc(e1));
592
593 exprNode_generateConstraints (e2);
594
595 e = doIf (e, e1, e2);
596
597
598 // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
599 break;
9280addf 600
601
616915dd 602 case XPR_IFELSE:
603 DPRINTF(("Starting IFELSE"));
604 // ret = message ("if (%s) %s else %s",
605 p = exprData_getTriplePred (data);
606 trueBranch = exprData_getTripleTrue (data);
607 falseBranch = exprData_getTripleFalse (data);
608
609 exprNode_exprTraverse (p,
610 FALSE, FALSE, exprNode_loc(p));
611 exprNode_generateConstraints (trueBranch);
612 exprNode_generateConstraints (falseBranch);
613
9280addf 614 p->ensuresConstraints = exprNode_traversEnsuresConstraints (p);
470b7798 615 p->requiresConstraints = exprNode_traversRequiresConstraints (p);
616
9280addf 617 p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p);
470b7798 618 p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p);
616915dd 619
470b7798 620 e = doIfElse (e, p, trueBranch, falseBranch);
616915dd 621 DPRINTF( ("Done IFELSE") );
622 break;
9280addf 623
616915dd 624 case XPR_DOWHILE:
470b7798 625
626 e2 = (exprData_getPairB (data));
627 e1 = (exprData_getPairA (data));
628
629 DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1) ) ));
630 exprNode_generateConstraints (e2);
631 exprNode_generateConstraints (e1);
632 e = exprNode_copyConstraints (e, e2);
633 DPRINTF ((message ("e = %s ", constraintList_print(e->requiresConstraints) ) ));
634
616915dd 635 break;
636
637 case XPR_BLOCK:
638 // ret = message ("{ %s }",
639 exprNode_generateConstraints (exprData_getSingle (data));
640 e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
641 e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
642 // e->constraints = (exprData_getSingle (data))->constraints;
643 break;
644
470b7798 645 case XPR_SWITCH:
646 e = doSwitch (e);
647 break;
616915dd 648 case XPR_STMT:
649 case XPR_STMTLIST:
650 return exprNode_stmtList (e);
651 /*@notreached@*/
652 break;
653 default:
654 ret=FALSE;
655 }
656 return ret;
657}
658
659bool lltok_isBoolean_Op (lltok tok)
660{
661 /*this should really be a switch statement but
662 I don't want to violate the abstraction
663 maybe this should go in lltok.c */
664
665 if (lltok_isEq_Op (tok) )
666 {
667 return TRUE;
668 }
669 if (lltok_isAnd_Op (tok) )
670
671 {
672
673 return TRUE;
674 }
675 if (lltok_isOr_Op (tok) )
676 {
677 return TRUE;
678 }
679
680 if (lltok_isGt_Op (tok) )
681 {
682 return TRUE;
683 }
684 if (lltok_isLt_Op (tok) )
685 {
686 return TRUE;
687 }
688
689 if (lltok_isLe_Op (tok) )
690 {
691 return TRUE;
692 }
693
694 if (lltok_isGe_Op (tok) )
695 {
696 return TRUE;
697 }
698
699 return FALSE;
700
701}
702
703
704void exprNode_booleanTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint)
705{
706 constraint cons;
707exprNode t1, t2;
708exprData data;
709lltok tok;
710constraintList tempList;
711data = e->edata;
712
713tok = exprData_getOpTok (data);
714
715
716t1 = exprData_getOpA (data);
717t2 = exprData_getOpB (data);
718
719
720/* arithmetic tests */
721
722if (lltok_isEq_Op (tok) )
723{
724 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
725 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
726}
727
728
729 if (lltok_isLt_Op (tok) )
730 {
731 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
732 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
733 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
734 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
735 }
736
737
738if (lltok_isGe_Op (tok) )
739{
740
741 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
742 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
743
744 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
745 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
746
747}
748
749
750 if (lltok_isGt_Op (tok) )
751{
752 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
753 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
754 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
755 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
756}
757
758if (lltok_isLe_Op (tok) )
759{
760 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
761 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
762
763 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
764 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
765}
766
767
768
769/*Logical operations */
770
771 if (lltok_isAnd_Op (tok) )
772
773 {
774 //true ensures
775 tempList = constraintList_copy (t1->trueEnsuresConstraints);
776 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
777 e->trueEnsuresConstraints = constraintList_addList(e->trueEnsuresConstraints, tempList);
778
779 //false ensures: fens t1 or tens t1 and fens t2
780 tempList = constraintList_copy (t1->trueEnsuresConstraints);
781 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
782 tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
783 e->falseEnsuresConstraints =constraintList_addList(e->falseEnsuresConstraints, tempList);
784
785 }
786
787 if (lltok_isOr_Op (tok) )
788 {
789 //false ensures
790 tempList = constraintList_copy (t1->falseEnsuresConstraints);
791 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
792 e->falseEnsuresConstraints = constraintList_addList(e->falseEnsuresConstraints, tempList);
793
794 //true ensures: tens t1 or fens t1 and tens t2
795 tempList = constraintList_copy (t1->falseEnsuresConstraints);
796 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
797 tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
798 e->trueEnsuresConstraints =constraintList_addList(e->trueEnsuresConstraints, tempList);
799
800 }
801
802}
803
804bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint)
805{
9280addf 806 exprNode t1, t2, fcn;
616915dd 807 lltok tok;
808 bool handledExprNode;
809 exprData data;
810 constraint cons;
811
470b7798 812 if (exprNode_isError(e) )
813 {
814 return FALSE;
815 }
816
817 DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
616915dd 818 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
470b7798 819
820 e->requiresConstraints = constraintList_new();
821 e->ensuresConstraints = constraintList_new();
822 e->trueEnsuresConstraints = constraintList_new();;
823 e->falseEnsuresConstraints = constraintList_new();;
824
825 if (exprNode_isUnhandled (e) )
616915dd 826 {
827 return FALSE;
828 }
829 // e = makeDataTypeConstraints (e);
830
831 handledExprNode = TRUE;
832
833 data = e->edata;
834
835 switch (e->kind)
836 {
837
838
839 case XPR_WHILEPRED:
840 t1 = exprData_getSingle (data);
841 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
842 e = exprNode_copyConstraints (e, t1);
843 break;
844
845 case XPR_FETCH:
846
847 if (definatelv )
848 {
849 t1 = (exprData_getPairA (data) );
850 t2 = (exprData_getPairB (data) );
851 cons = constraint_makeWriteSafeExprNode (t1, t2);
852 }
853 else
854 {
855 t1 = (exprData_getPairA (data) );
856 t2 = (exprData_getPairB (data) );
857 cons = constraint_makeReadSafeExprNode (t1, t2 );
858 }
859
860 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
861 cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
862 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
863
9280addf 864 cons = constraint_makeEnsureLteMaxRead (t2, t1);
616915dd 865 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
866
867 // cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
868 // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
869
870 exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
871 exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
872
873 /*@i325 Should check which is array/index. */
874 break;
875
876 case XPR_PARENS:
877 exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
878 // e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
879 break;
880 case XPR_INIT:
881 /* //t1 = exprData_getInitId (data); */
882 t2 = exprData_getInitNode (data);
883 //exprNode_exprTraverse (t1, TRUE, FALSE, sequencePoint );
884
885 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
886
887 /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
888 if ( (!exprNode_isError (e)) && (!exprNode_isError(t2)) )
889 {
890 cons = constraint_makeEnsureEqual (e, t2, sequencePoint);
891 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
892 }
893
894 break;
895 case XPR_ASSIGN:
896 t1 = exprData_getOpA (data);
897 t2 = exprData_getOpB (data);
898 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
899 lltok_unparse (exprData_getOpTok (data));
900 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
901
902 /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
903 if ( (!exprNode_isError (t1)) && (!exprNode_isError(t2)) )
904 {
905 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
906 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
907 }
908 break;
909 case XPR_OP:
910 t1 = exprData_getOpA (data);
911 t2 = exprData_getOpB (data);
912
913 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
914 tok = exprData_getOpTok (data);
915 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
916
917 if (lltok_isBoolean_Op (tok) )
918 exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
919
920 // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
921 break;
922 case XPR_SIZEOFT:
923 ctype_unparse (qtype_getType (exprData_getType (data) ) );
924
925 break;
926
927 case XPR_SIZEOF:
928 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
929 // e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
930 break;
931
932 case XPR_CALL:
9280addf 933 fcn = exprData_getFcn(data);
934
935 exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint );
616915dd 936 exprNodeList_unparse (exprData_getArgs (data) );
9280addf 937 DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data) ) ) ) );
616915dd 938
9280addf 939 fcn->requiresConstraints = constraintList_addList (fcn->requiresConstraints,
940 checkCall (fcn, exprData_getArgs (data) ) );
616915dd 941
9280addf 942 fcn->ensuresConstraints = constraintList_addList (fcn->ensuresConstraints,
943 getPostConditions(fcn, exprData_getArgs (data),e ) );
944
945 t1 = exprNode_createNew (exprNode_getType (e) );
946
947 checkArgumentList (t1, exprData_getArgs(data), sequencePoint);
616915dd 948
9280addf 949
950 mergeResolve (e, t1, fcn);
951
616915dd 952 // e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) );
953 break;
954
955 case XPR_RETURN:
956 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
957 break;
958
959 case XPR_NULLRETURN:
960 cstring_makeLiteral ("return");;
961 break;
962
963
964 case XPR_FACCESS:
965 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
966 exprData_getFieldName (data) ;
967 break;
968
969 case XPR_ARROW:
970 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
971 exprData_getFieldName (data);
972 break;
973
974 case XPR_STRINGLITERAL:
975 cstring_copy (exprData_getLiteral (data));
976 break;
977
978 case XPR_NUMLIT:
979 cstring_copy (exprData_getLiteral (data));
980 break;
981
982 case XPR_PREOP:
983 t1 = exprData_getUopNode(data);
984 tok = (exprData_getUopTok (data));
985 //lltok_unparse (exprData_getUopTok (data));
986 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
987 /*handle * pointer access */
988 if (lltok_isInc_Op (tok) )
989 {
990 DPRINTF(("doing ++(var)"));
991 t1 = exprData_getUopNode (data);
992 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
993 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
994 }
995 else if (lltok_isDec_Op (tok) )
996 {
997 DPRINTF(("doing --(var)"));
998 t1 = exprData_getUopNode (data);
999 cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1000 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1001 }
1002
1003 if (lltok_isMult( exprData_getUopTok (data) ) )
1004 {
1005 if (definatelv)
1006 {
1007 cons = constraint_makeWriteSafeInt (t1, 0);
1008 }
1009 else
1010 {
1011 cons = constraint_makeReadSafeInt (t1, 0);
1012 }
1013 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1014 }
1015
1016 /* ! expr */
1017 if (lltok_isNot_Op (exprData_getUopTok (data) ) )
1018 {
1019 e->trueEnsuresConstraints = constraintList_copy (t1->falseEnsuresConstraints);
1020 e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
1021 }
1022 break;
1023
1024 case XPR_POSTOP:
1025
1026 exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
1027 lltok_unparse (exprData_getUopTok (data));
1028 if (lltok_isInc_Op (exprData_getUopTok (data) ) )
1029 {
1030 DPRINTF(("doing ++"));
1031 t1 = exprData_getUopNode (data);
1032 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
1033 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1034 }
1035 if (lltok_isDec_Op (exprData_getUopTok (data) ) )
1036 {
1037 DPRINTF(("doing --"));
1038 t1 = exprData_getUopNode (data);
1039 cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1040 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1041 }
1042 break;
470b7798 1043 case XPR_CAST:
1044 llassert(FALSE);
1045 exprNode_exprTraverse (exprData_getCastNode (data), definatelv, definaterv, sequencePoint );
1046 break;
1047 case XPR_COND:
1048 {
1049 exprNode pred, true, false;
1050 llassert(FALSE);
1051 pred = exprData_getTriplePred (data);
1052 true = exprData_getTripleTrue (data);
1053 false = exprData_getTripleFalse (data);
1054
1055 exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint );
1056 pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
1057 pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
1058
1059 pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred);
1060 pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
1061
1062 exprNode_exprTraverse (true, FALSE, TRUE, sequencePoint );
1063 true->ensuresConstraints = exprNode_traversEnsuresConstraints(true);
1064 true->requiresConstraints = exprNode_traversRequiresConstraints(true);
1065
1066 true->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(true);
1067 true->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(true);
1068
1069 exprNode_exprTraverse (false, FALSE, TRUE, sequencePoint );
1070 false->ensuresConstraints = exprNode_traversEnsuresConstraints(false);
1071 false->requiresConstraints = exprNode_traversRequiresConstraints(false);
1072
1073 false->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(false);
1074 false->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(false);
1075
1076
1077 /* if pred is true e equals true otherwise pred equals false */
1078
1079 cons = constraint_makeEnsureEqual (e, true, sequencePoint);
1080 true->ensuresConstraints = constraintList_add(true->ensuresConstraints, cons);
1081
1082 cons = constraint_makeEnsureEqual (e, true, sequencePoint);
1083 false->ensuresConstraints = constraintList_add(false->ensuresConstraints, cons);
1084
1085 e = doIfElse (e, pred, true, false);
1086
1087 }
1088 break;
1089 case XPR_COMMA:
1090 llassert(FALSE);
1091 t1 = exprData_getPairA (data);
1092 t2 = exprData_getPairB (data);
1093 /* we essiantially treat this like expr1; expr2
1094 of course sequencePoint isn't adjusted so this isn't completely accurate
1095 problems../ */
1096 exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint );
1097 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1098 mergeResolve (e, t1, t2);
1099 break;
1100
616915dd 1101 default:
1102 handledExprNode = FALSE;
1103 }
1104
1105 e->requiresConstraints = constraintList_preserveOrig ( e->requiresConstraints);
1106 e->ensuresConstraints = constraintList_preserveOrig ( e->ensuresConstraints);
9280addf 1107 e->requiresConstraints = constraintList_addGeneratingExpr ( e->requiresConstraints, e);
1108
1109 e->ensuresConstraints = constraintList_addGeneratingExpr ( e->ensuresConstraints, e);
1110
1111 DPRINTF((message ("ensures constraint for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
616915dd 1112
1113 return handledExprNode;
1114}
1115
1116
1117constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
1118{
470b7798 1119 exprNode t1;
616915dd 1120
1121 bool handledExprNode;
1122 // char * mes;
1123 exprData data;
1124 constraintList ret;
1125
1126 if (exprNode_handleError (e))
1127 {
1128 ret = constraintList_new();
1129 return ret;
1130 }
1131 ret = constraintList_copy (e->trueEnsuresConstraints );
1132
1133 handledExprNode = TRUE;
1134
1135 data = e->edata;
1136
1137 switch (e->kind)
1138 {
9280addf 1139 case XPR_WHILEPRED:
1140 t1 = exprData_getSingle (data);
1141 ret = constraintList_addList ( ret,exprNode_traversTrueEnsuresConstraints (t1) );
1142 break;
616915dd 1143
1144 case XPR_FETCH:
1145
1146 ret = constraintList_addList (ret,
1147 exprNode_traversTrueEnsuresConstraints
1148 (exprData_getPairA (data) ) );
1149
1150 ret = constraintList_addList (ret,
1151 exprNode_traversTrueEnsuresConstraints
1152 (exprData_getPairB (data) ) );
1153 break;
1154 case XPR_PREOP:
1155
1156 ret = constraintList_addList (ret,
1157 exprNode_traversTrueEnsuresConstraints
1158 (exprData_getUopNode (data) ) );
1159 break;
1160
1161 case XPR_PARENS:
1162 ret = constraintList_addList (ret, exprNode_traversTrueEnsuresConstraints
1163 (exprData_getUopNode (data) ) );
1164 break;
1165 case XPR_ASSIGN:
1166 ret = constraintList_addList (ret,
1167 exprNode_traversTrueEnsuresConstraints
1168 (exprData_getOpA (data) ) );
1169
1170 ret = constraintList_addList (ret,
1171 exprNode_traversTrueEnsuresConstraints
1172 (exprData_getOpB (data) ) );
1173 break;
1174 case XPR_OP:
1175 ret = constraintList_addList (ret,
1176 exprNode_traversTrueEnsuresConstraints
1177 (exprData_getOpA (data) ) );
1178
1179 ret = constraintList_addList (ret,
1180 exprNode_traversTrueEnsuresConstraints
1181 (exprData_getOpB (data) ) );
1182 break;
1183 case XPR_SIZEOFT:
1184
1185 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1186
1187 break;
1188
1189 case XPR_SIZEOF:
1190
1191 ret = constraintList_addList (ret,
1192 exprNode_traversTrueEnsuresConstraints
1193 (exprData_getSingle (data) ) );
1194 break;
1195
1196 case XPR_CALL:
1197 ret = constraintList_addList (ret,
1198 exprNode_traversTrueEnsuresConstraints
1199 (exprData_getFcn (data) ) );
1200 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1201 break;
1202
1203 case XPR_RETURN:
1204 ret = constraintList_addList (ret,
1205 exprNode_traversTrueEnsuresConstraints
1206 (exprData_getSingle (data) ) );
1207 break;
1208
1209 case XPR_NULLRETURN:
1210 // cstring_makeLiteral ("return");;
1211 break;
1212
1213 case XPR_FACCESS:
1214 ret = constraintList_addList (ret,
1215 exprNode_traversTrueEnsuresConstraints
1216 (exprData_getFieldNode (data) ) );
1217 //exprData_getFieldName (data) ;
1218 break;
1219
1220 case XPR_ARROW:
1221 ret = constraintList_addList (ret,
1222 exprNode_traversTrueEnsuresConstraints
1223 (exprData_getFieldNode (data) ) );
1224 // exprData_getFieldName (data);
1225 break;
1226
1227 case XPR_STRINGLITERAL:
1228 // cstring_copy (exprData_getLiteral (data));
1229 break;
1230
1231 case XPR_NUMLIT:
1232 // cstring_copy (exprData_getLiteral (data));
1233 break;
1234 case XPR_POSTOP:
1235
1236 ret = constraintList_addList (ret,
1237 exprNode_traversTrueEnsuresConstraints
1238 (exprData_getUopNode (data) ) );
1239 break;
470b7798 1240
1241 case XPR_CAST:
1242
1243 ret = constraintList_addList (ret,
1244 exprNode_traversTrueEnsuresConstraints
1245 (exprData_getCastNode (data) ) );
1246 break;
1247
1248 break;
616915dd 1249 default:
1250 break;
1251 }
1252
1253 return ret;
1254}
1255
9280addf 1256constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
1257{
470b7798 1258 exprNode t1;
9280addf 1259
1260 bool handledExprNode;
1261 // char * mes;
1262 exprData data;
1263 constraintList ret;
1264
1265 if (exprNode_handleError (e))
1266 {
1267 ret = constraintList_new();
1268 return ret;
1269 }
1270 ret = constraintList_copy (e->falseEnsuresConstraints );
1271
1272 handledExprNode = TRUE;
1273
1274 data = e->edata;
1275
1276 switch (e->kind)
1277 {
1278 case XPR_WHILEPRED:
1279 t1 = exprData_getSingle (data);
1280 ret = constraintList_addList ( ret,exprNode_traversFalseEnsuresConstraints (t1) );
1281 break;
1282
1283 case XPR_FETCH:
1284
1285 ret = constraintList_addList (ret,
1286 exprNode_traversFalseEnsuresConstraints
1287 (exprData_getPairA (data) ) );
1288
1289 ret = constraintList_addList (ret,
1290 exprNode_traversFalseEnsuresConstraints
1291 (exprData_getPairB (data) ) );
1292 break;
1293 case XPR_PREOP:
1294
1295 ret = constraintList_addList (ret,
1296 exprNode_traversFalseEnsuresConstraints
1297 (exprData_getUopNode (data) ) );
1298 break;
1299
1300 case XPR_PARENS:
1301 ret = constraintList_addList (ret, exprNode_traversFalseEnsuresConstraints
1302 (exprData_getUopNode (data) ) );
1303 break;
1304 case XPR_ASSIGN:
1305 ret = constraintList_addList (ret,
1306 exprNode_traversFalseEnsuresConstraints
1307 (exprData_getOpA (data) ) );
1308
1309 ret = constraintList_addList (ret,
1310 exprNode_traversFalseEnsuresConstraints
1311 (exprData_getOpB (data) ) );
1312 break;
1313 case XPR_OP:
1314 ret = constraintList_addList (ret,
1315 exprNode_traversFalseEnsuresConstraints
1316 (exprData_getOpA (data) ) );
1317
1318 ret = constraintList_addList (ret,
1319 exprNode_traversFalseEnsuresConstraints
1320 (exprData_getOpB (data) ) );
1321 break;
1322 case XPR_SIZEOFT:
1323
1324 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1325
1326 break;
1327
1328 case XPR_SIZEOF:
1329
1330 ret = constraintList_addList (ret,
1331 exprNode_traversFalseEnsuresConstraints
1332 (exprData_getSingle (data) ) );
1333 break;
1334
1335 case XPR_CALL:
1336 ret = constraintList_addList (ret,
1337 exprNode_traversFalseEnsuresConstraints
1338 (exprData_getFcn (data) ) );
1339 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1340 break;
1341
1342 case XPR_RETURN:
1343 ret = constraintList_addList (ret,
1344 exprNode_traversFalseEnsuresConstraints
1345 (exprData_getSingle (data) ) );
1346 break;
1347
1348 case XPR_NULLRETURN:
1349 // cstring_makeLiteral ("return");;
1350 break;
1351
1352 case XPR_FACCESS:
1353 ret = constraintList_addList (ret,
1354 exprNode_traversFalseEnsuresConstraints
1355 (exprData_getFieldNode (data) ) );
1356 //exprData_getFieldName (data) ;
1357 break;
1358
1359 case XPR_ARROW:
1360 ret = constraintList_addList (ret,
1361 exprNode_traversFalseEnsuresConstraints
1362 (exprData_getFieldNode (data) ) );
1363 // exprData_getFieldName (data);
1364 break;
1365
1366 case XPR_STRINGLITERAL:
1367 // cstring_copy (exprData_getLiteral (data));
1368 break;
1369
1370 case XPR_NUMLIT:
1371 // cstring_copy (exprData_getLiteral (data));
1372 break;
1373 case XPR_POSTOP:
1374
1375 ret = constraintList_addList (ret,
1376 exprNode_traversFalseEnsuresConstraints
1377 (exprData_getUopNode (data) ) );
1378 break;
470b7798 1379
1380 case XPR_CAST:
1381
1382 ret = constraintList_addList (ret,
1383 exprNode_traversFalseEnsuresConstraints
1384 (exprData_getCastNode (data) ) );
1385 break;
1386
9280addf 1387 default:
1388 break;
1389 }
1390
1391 return ret;
1392}
1393
616915dd 1394
1395/* walk down the tree and get all requires Constraints in each subexpression*/
1396constraintList exprNode_traversRequiresConstraints (exprNode e)
1397{
470b7798 1398 exprNode t1;
616915dd 1399
1400 bool handledExprNode;
1401 // char * mes;
1402 exprData data;
1403 constraintList ret;
1404
1405 if (exprNode_handleError (e))
1406 {
1407 ret = constraintList_new();
1408 return ret;
1409 }
1410 ret = constraintList_copy (e->requiresConstraints );
1411
1412 handledExprNode = TRUE;
1413
1414 data = e->edata;
1415
1416 switch (e->kind)
1417 {
9280addf 1418 case XPR_WHILEPRED:
1419 t1 = exprData_getSingle (data);
1420 ret = constraintList_addList ( ret,exprNode_traversRequiresConstraints (t1) );
1421 break;
616915dd 1422
1423 case XPR_FETCH:
1424
1425 ret = constraintList_addList (ret,
1426 exprNode_traversRequiresConstraints
1427 (exprData_getPairA (data) ) );
1428
1429 ret = constraintList_addList (ret,
1430 exprNode_traversRequiresConstraints
1431 (exprData_getPairB (data) ) );
1432 break;
1433 case XPR_PREOP:
1434
1435 ret = constraintList_addList (ret,
1436 exprNode_traversRequiresConstraints
1437 (exprData_getUopNode (data) ) );
1438 break;
1439
1440 case XPR_PARENS:
1441 ret = constraintList_addList (ret, exprNode_traversRequiresConstraints
1442 (exprData_getUopNode (data) ) );
1443 break;
1444 case XPR_ASSIGN:
1445 ret = constraintList_addList (ret,
1446 exprNode_traversRequiresConstraints
1447 (exprData_getOpA (data) ) );
1448
1449 ret = constraintList_addList (ret,
1450 exprNode_traversRequiresConstraints
1451 (exprData_getOpB (data) ) );
1452 break;
1453 case XPR_OP:
1454 ret = constraintList_addList (ret,
1455 exprNode_traversRequiresConstraints
1456 (exprData_getOpA (data) ) );
1457
1458 ret = constraintList_addList (ret,
1459 exprNode_traversRequiresConstraints
1460 (exprData_getOpB (data) ) );
1461 break;
1462 case XPR_SIZEOFT:
1463
1464 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1465
1466 break;
1467
1468 case XPR_SIZEOF:
1469
1470 ret = constraintList_addList (ret,
1471 exprNode_traversRequiresConstraints
1472 (exprData_getSingle (data) ) );
1473 break;
1474
1475 case XPR_CALL:
1476 ret = constraintList_addList (ret,
1477 exprNode_traversRequiresConstraints
1478 (exprData_getFcn (data) ) );
1479 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1480 break;
1481
1482 case XPR_RETURN:
1483 ret = constraintList_addList (ret,
1484 exprNode_traversRequiresConstraints
1485 (exprData_getSingle (data) ) );
1486 break;
1487
1488 case XPR_NULLRETURN:
1489 // cstring_makeLiteral ("return");;
1490 break;
1491
1492 case XPR_FACCESS:
1493 ret = constraintList_addList (ret,
1494 exprNode_traversRequiresConstraints
1495 (exprData_getFieldNode (data) ) );
1496 //exprData_getFieldName (data) ;
1497 break;
1498
1499 case XPR_ARROW:
1500 ret = constraintList_addList (ret,
1501 exprNode_traversRequiresConstraints
1502 (exprData_getFieldNode (data) ) );
1503 // exprData_getFieldName (data);
1504 break;
1505
1506 case XPR_STRINGLITERAL:
1507 // cstring_copy (exprData_getLiteral (data));
1508 break;
1509
1510 case XPR_NUMLIT:
1511 // cstring_copy (exprData_getLiteral (data));
1512 break;
1513 case XPR_POSTOP:
1514
1515 ret = constraintList_addList (ret,
1516 exprNode_traversRequiresConstraints
1517 (exprData_getUopNode (data) ) );
1518 break;
470b7798 1519
1520 case XPR_CAST:
1521
1522 ret = constraintList_addList (ret,
1523 exprNode_traversRequiresConstraints
1524 (exprData_getCastNode (data) ) );
1525 break;
1526
616915dd 1527 default:
1528 break;
1529 }
1530
1531 return ret;
1532}
1533
1534
1535/* walk down the tree and get all Ensures Constraints in each subexpression*/
1536constraintList exprNode_traversEnsuresConstraints (exprNode e)
1537{
470b7798 1538 exprNode t1;
616915dd 1539
1540 bool handledExprNode;
1541 // char * mes;
1542 exprData data;
1543 // constraintExpr tmp;
1544 // constraint cons;
1545 constraintList ret;
1546
1547
1548 if (exprNode_handleError (e))
1549 {
1550 ret = constraintList_new();
1551 return ret;
1552 }
1553
1554 ret = constraintList_copy (e->ensuresConstraints );
1555 handledExprNode = TRUE;
1556
1557 data = e->edata;
1558
1559 DPRINTF( (message (
1560 "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
1561 exprNode_unparse (e),
1562 constraintList_print(e->ensuresConstraints)
1563 )
1564 ));
1565
1566
1567 switch (e->kind)
1568 {
9280addf 1569 case XPR_WHILEPRED:
1570 t1 = exprData_getSingle (data);
1571 ret = constraintList_addList ( ret,exprNode_traversEnsuresConstraints (t1) );
1572 break;
616915dd 1573
1574 case XPR_FETCH:
1575
1576 ret = constraintList_addList (ret,
1577 exprNode_traversEnsuresConstraints
1578 (exprData_getPairA (data) ) );
1579
1580 ret = constraintList_addList (ret,
1581 exprNode_traversEnsuresConstraints
1582 (exprData_getPairB (data) ) );
1583 break;
1584 case XPR_PREOP:
1585
1586 ret = constraintList_addList (ret,
1587 exprNode_traversEnsuresConstraints
1588 (exprData_getUopNode (data) ) );
1589 break;
1590
1591 case XPR_PARENS:
1592 ret = constraintList_addList (ret, exprNode_traversEnsuresConstraints
1593 (exprData_getUopNode (data) ) );
1594 break;
1595 case XPR_ASSIGN:
1596 ret = constraintList_addList (ret,
1597 exprNode_traversEnsuresConstraints
1598 (exprData_getOpA (data) ) );
1599
1600 ret = constraintList_addList (ret,
1601 exprNode_traversEnsuresConstraints
1602 (exprData_getOpB (data) ) );
1603 break;
1604 case XPR_OP:
1605 ret = constraintList_addList (ret,
1606 exprNode_traversEnsuresConstraints
1607 (exprData_getOpA (data) ) );
1608
1609 ret = constraintList_addList (ret,
1610 exprNode_traversEnsuresConstraints
1611 (exprData_getOpB (data) ) );
1612 break;
1613 case XPR_SIZEOFT:
1614
1615 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1616
1617 break;
1618
1619 case XPR_SIZEOF:
1620
1621 ret = constraintList_addList (ret,
1622 exprNode_traversEnsuresConstraints
1623 (exprData_getSingle (data) ) );
1624 break;
1625
1626 case XPR_CALL:
1627 ret = constraintList_addList (ret,
1628 exprNode_traversEnsuresConstraints
1629 (exprData_getFcn (data) ) );
1630 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1631 break;
1632
1633 case XPR_RETURN:
1634 ret = constraintList_addList (ret,
1635 exprNode_traversEnsuresConstraints
1636 (exprData_getSingle (data) ) );
1637 break;
1638
1639 case XPR_NULLRETURN:
1640 // cstring_makeLiteral ("return");;
1641 break;
1642
1643 case XPR_FACCESS:
1644 ret = constraintList_addList (ret,
1645 exprNode_traversEnsuresConstraints
1646 (exprData_getFieldNode (data) ) );
1647 //exprData_getFieldName (data) ;
1648 break;
1649
1650 case XPR_ARROW:
1651 ret = constraintList_addList (ret,
1652 exprNode_traversEnsuresConstraints
1653 (exprData_getFieldNode (data) ) );
1654 // exprData_getFieldName (data);
1655 break;
1656
1657 case XPR_STRINGLITERAL:
1658 // cstring_copy (exprData_getLiteral (data));
1659 break;
1660
1661 case XPR_NUMLIT:
1662 // cstring_copy (exprData_getLiteral (data));
1663 break;
1664 case XPR_POSTOP:
1665
1666 ret = constraintList_addList (ret,
1667 exprNode_traversEnsuresConstraints
1668 (exprData_getUopNode (data) ) );
1669 break;
470b7798 1670 case XPR_CAST:
1671
1672 ret = constraintList_addList (ret,
1673 exprNode_traversEnsuresConstraints
1674 (exprData_getCastNode (data) ) );
1675 break;
1676
616915dd 1677 default:
1678 break;
1679 }
1680DPRINTF( (message (
1681 "exprnode_traversEnsuresConstraints call for %s with constraintList of is returning %s",
1682 exprNode_unparse (e),
1683 // constraintList_print(e->ensuresConstraints),
1684 constraintList_print(ret)
1685 )
1686 ));
1687
1688
1689 return ret;
1690}
1691
git-cvsimport mirror of splint
This page took 0.277435 seconds and 5 git commands to generate.