]> andersk Git - splint.git/blame - src/constraintGeneration.c
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Updating for cert move
[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
c3e695ff 121 e->requiresConstraints = constraintList_makeNew();
122 e->ensuresConstraints = constraintList_makeNew();
123 e->trueEnsuresConstraints = constraintList_makeNew();
124 e->falseEnsuresConstraints = constraintList_makeNew();
9280addf 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 }
c3e695ff 206 e->requiresConstraints = constraintList_makeNew();
207 e->ensuresConstraints = constraintList_makeNew();
616915dd 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
c3e695ff 279 e->requiresConstraints = constraintList_makeNew();
280 e->ensuresConstraints = constraintList_makeNew();
616915dd 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
c3e695ff 324 test->trueEnsuresConstraints = constraintList_substitute(test->trueEnsuresConstraints, test->ensuresConstraints);
325
326 DPRINTF ((message ("doIf: test ensures %s ", constraintList_print(test->ensuresConstraints) ) ) );
327
328 DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints) ) ) );
329
616915dd 330 e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints);
331 e->requiresConstraints = reflectChanges (e->requiresConstraints,
332 test->ensuresConstraints);
470b7798 333 e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints);
334
616915dd 335#warning bad
336 e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
90bc41f7 337
338 if (exprNode_mayEscape (body) )
339 {
340 DPRINTF (( message("doIf: the if statement body %s returns or exits", exprNode_unparse(body) ) ));
341 e->ensuresConstraints = constraintList_mergeEnsures (e->ensuresConstraints,
470b7798 342 test->falseEnsuresConstraints);
90bc41f7 343 }
344
9280addf 345 DPRINTF ((message ("doIf: if requiers %s ", constraintList_print(e->requiresConstraints) ) ) );
346
616915dd 347 return e;
348}
349
470b7798 350/*drl added 3/4/2001
351 Also used for condition i.e. ?: operation
352
353 Precondition
354 This function assumes that p, trueBranch, falseBranch have have all been traversed
355 for constraints i.e. we assume that exprNode_traversEnsuresConstraints,
356 exprNode_traversRequiresConstraints, exprNode_traversTrueEnsuresConstraints,
357 exprNode_traversFalseEnsuresConstraints have all been run
358*/
359
360
361exprNode doIfElse (/*@returned@*/ exprNode e, exprNode p, exprNode trueBranch, exprNode falseBranch)
362{
363
364 constraintList c1, cons, t, f;
365
366 // do requires clauses
367 c1 = constraintList_copy (p->ensuresConstraints);
368
369 t = reflectChanges (trueBranch->requiresConstraints, p->trueEnsuresConstraints);
370 t = reflectChanges (t, p->ensuresConstraints);
371
372 // e->requiresConstraints = constraintList_copy (cons);
373
374 cons = reflectChanges (falseBranch->requiresConstraints, p->falseEnsuresConstraints);
375 cons = reflectChanges (cons, c1);
376
377 e->requiresConstraints = constraintList_mergeRequires (t, cons);
378 e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, p->requiresConstraints);
379
380 // do ensures clauses
381 // find the the ensures lists for each subbranch
382 t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
383 t = constraintList_mergeEnsures (p->ensuresConstraints, t);
384
385 f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
386 f = constraintList_mergeEnsures (p->ensuresConstraints, f);
387
388 // find ensures for whole if/else statement
389
390 e->ensuresConstraints = constraintList_logicalOr (t, f);
391
392 return e;
393}
9280addf 394
395exprNode doWhile (exprNode e, exprNode test, exprNode body)
396{
397 DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e) ) ) );
398 return doIf (e, test, body);
399}
400
616915dd 401constraintList constraintList_makeFixedArrayConstraints (sRefSet s)
402{
403 constraintList ret;
470b7798 404 constraint con;
c3e695ff 405 ret = constraintList_makeNew();
616915dd 406
407 sRefSet_elements (s, el)
408 {
409 // llassert (el);
410 if (sRef_isFixedArray(el) )
411 {
412 int s;
470b7798 413 DPRINTF( (message("%s is a fixed array",
414 sRef_unparse(el)) ) );
415 //if (el->kind == SK_DERIVED)
416 // break; //hack until I find the real problem
616915dd 417 s = sRef_getArraySize(el);
418 DPRINTF( (message("%s is a fixed array with size %d",
419 sRef_unparse(el), s) ) );
420 con = constraint_makeSRefSetBufferSize (el, (s - 1));
421 //con = constraint_makeSRefWriteSafeInt (el, (s - 1));
422 ret = constraintList_add(ret, con);
423 }
424 else
425 {
426 DPRINTF( (message("%s is not a fixed array",
427 sRef_unparse(el)) ) );
470b7798 428
429
430 if (sRef_isExternallyVisible (el) )
431 {
432 /*DPRINTF( (message("%s is externally visible",
433 sRef_unparse(el) ) ));
434 con = constraint_makeSRefWriteSafeInt(el, 0);
435 ret = constraintList_add(ret, con);
436
437 con = constraint_makeSRefReadSafeInt(el, 0);
438
439 ret = constraintList_add(ret, con);*/
440 }
616915dd 441 }
442 }
443 end_sRefSet_elements
444
470b7798 445 DPRINTF(( message("constraintList_makeFixedArrayConstraints returning %s",
446 constraintList_print(ret) ) ));
616915dd 447 return ret;
448}
449
450exprNode makeDataTypeConstraints (exprNode e)
451{
452 constraintList c;
453 DPRINTF(("makeDataTypeConstraints"));
454
455 c = constraintList_makeFixedArrayConstraints (e->uses);
456
457 e->ensuresConstraints = constraintList_addList (e->ensuresConstraints, c);
458
459 return e;
460}
461
462void doFor (exprNode e, exprNode forPred, exprNode forBody)
463{
464 exprNode init, test, inc;
465 //merge the constraints: modle as if statement
466 /* init
467 if (test)
468 for body
469 inc */
470 init = exprData_getTripleInit (forPred->edata);
471 test = exprData_getTripleTest (forPred->edata);
472 inc = exprData_getTripleInc (forPred->edata);
473
474 if ( ( (exprNode_isError (test) /*|| (exprNode_isError(init) )*/ ) || (exprNode_isError (inc) ) ) )
475 {
476 DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e) ) ) );
477 return;
478 }
479
480 forLoopHeuristics(e, forPred, forBody);
481
482 e->requiresConstraints = reflectChanges (forBody->requiresConstraints, test->ensuresConstraints);
483 e->requiresConstraints = reflectChanges (e->requiresConstraints, test->trueEnsuresConstraints);
484 e->requiresConstraints = reflectChanges (e->requiresConstraints, forPred->ensuresConstraints);
485
486 if (!forBody->canBreak)
487 {
488 e->ensuresConstraints = constraintList_addList(e->ensuresConstraints, forPred->ensuresConstraints);
489 e->ensuresConstraints = constraintList_addList(e->ensuresConstraints, test->falseEnsuresConstraints);
490 }
491 else
492 {
493 DPRINTF(("Can break") );
494 }
495
496}
497
470b7798 498exprNode doSwitch (/*@returned@*/ exprNode e)
499{
500 exprNode body;
501 exprData data;
502
503 data = e->edata;
504 llassert(FALSE);
90bc41f7 505 //DPRINTF (( message ("doSwitch for: switch (%s) %s",
470b7798 506 // exprNode_unparse (exprData_getPairA (data)),
507 // exprNode_unparse (exprData_getPairB (data))) ));
508
509 body = exprData_getPairB (data);
510
511 // exprNode_generateConstraints(body);
512
513 // e->requiresConstraints = constraintList_copy ( body->requiresConstraints );
514 //e->ensuresConstraints = constraintList_copy ( body->ensuresConstraints );
515
516 return e;
517}
9280addf 518
519
616915dd 520bool exprNode_multiStatement (exprNode e)
521{
522
523 bool ret;
524 exprData data;
525 exprNode e1, e2;
526 exprNode p, trueBranch, falseBranch;
527 exprNode forPred, forBody;
470b7798 528 exprNode test;
529 // constraintList t, f;
c3e695ff 530 e->requiresConstraints = constraintList_makeNew();
531 e->ensuresConstraints = constraintList_makeNew();
532 e->trueEnsuresConstraints = constraintList_makeNew();
533 e->falseEnsuresConstraints = constraintList_makeNew();
616915dd 534
535 // e = makeDataTypeConstraints(e);
536
537 DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
538 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
539
540 if (exprNode_handleError (e))
541 {
542 return FALSE;
543 }
544
545 data = e->edata;
546
547 ret = TRUE;
548
549 switch (e->kind)
550 {
551
552 case XPR_FOR:
553 // ret = message ("%s %s",
554 forPred = exprData_getPairA (data);
555 forBody = exprData_getPairB (data);
556
557 //first generate the constraints
558 exprNode_generateConstraints (forPred);
559 exprNode_generateConstraints (forBody);
560
561
562 doFor (e, forPred, forBody);
563
564 break;
565
566 case XPR_FORPRED:
567 // ret = message ("for (%s; %s; %s)",
568 exprNode_generateConstraints (exprData_getTripleInit (data) );
569 test = exprData_getTripleTest (data);
570 exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
9280addf 571 exprNode_generateConstraints (exprData_getTripleInc (data) );
572
616915dd 573 if (!exprNode_isError(test) )
574 test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
575
576 exprNode_generateConstraints (exprData_getTripleInc (data));
577 break;
9280addf 578
579 case XPR_WHILE:
580 e1 = exprData_getPairA (data);
581 e2 = exprData_getPairB (data);
582
583 exprNode_exprTraverse (e1,
584 FALSE, FALSE, exprNode_loc(e1));
585
586 exprNode_generateConstraints (e2);
587
588 e = doWhile (e, e1, e2);
589
590 break;
591
616915dd 592 case XPR_IF:
593 DPRINTF(( "IF:") );
594 DPRINTF ((exprNode_unparse(e) ) );
595 // ret = message ("if (%s) %s",
596 e1 = exprData_getPairA (data);
597 e2 = exprData_getPairB (data);
598
599 exprNode_exprTraverse (e1,
600 FALSE, FALSE, exprNode_loc(e1));
601
602 exprNode_generateConstraints (e2);
603
604 e = doIf (e, e1, e2);
605
606
607 // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
608 break;
9280addf 609
610
616915dd 611 case XPR_IFELSE:
612 DPRINTF(("Starting IFELSE"));
613 // ret = message ("if (%s) %s else %s",
614 p = exprData_getTriplePred (data);
615 trueBranch = exprData_getTripleTrue (data);
616 falseBranch = exprData_getTripleFalse (data);
617
618 exprNode_exprTraverse (p,
619 FALSE, FALSE, exprNode_loc(p));
620 exprNode_generateConstraints (trueBranch);
621 exprNode_generateConstraints (falseBranch);
622
9280addf 623 p->ensuresConstraints = exprNode_traversEnsuresConstraints (p);
470b7798 624 p->requiresConstraints = exprNode_traversRequiresConstraints (p);
625
9280addf 626 p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p);
470b7798 627 p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p);
616915dd 628
470b7798 629 e = doIfElse (e, p, trueBranch, falseBranch);
616915dd 630 DPRINTF( ("Done IFELSE") );
631 break;
9280addf 632
616915dd 633 case XPR_DOWHILE:
470b7798 634
635 e2 = (exprData_getPairB (data));
636 e1 = (exprData_getPairA (data));
637
638 DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1) ) ));
639 exprNode_generateConstraints (e2);
640 exprNode_generateConstraints (e1);
641 e = exprNode_copyConstraints (e, e2);
642 DPRINTF ((message ("e = %s ", constraintList_print(e->requiresConstraints) ) ));
643
616915dd 644 break;
645
646 case XPR_BLOCK:
647 // ret = message ("{ %s }",
648 exprNode_generateConstraints (exprData_getSingle (data));
649 e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
650 e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
651 // e->constraints = (exprData_getSingle (data))->constraints;
652 break;
653
470b7798 654 case XPR_SWITCH:
655 e = doSwitch (e);
656 break;
616915dd 657 case XPR_STMT:
658 case XPR_STMTLIST:
659 return exprNode_stmtList (e);
660 /*@notreached@*/
661 break;
662 default:
663 ret=FALSE;
664 }
665 return ret;
666}
667
668bool lltok_isBoolean_Op (lltok tok)
669{
670 /*this should really be a switch statement but
671 I don't want to violate the abstraction
672 maybe this should go in lltok.c */
673
674 if (lltok_isEq_Op (tok) )
675 {
676 return TRUE;
677 }
678 if (lltok_isAnd_Op (tok) )
679
680 {
681
682 return TRUE;
683 }
684 if (lltok_isOr_Op (tok) )
685 {
686 return TRUE;
687 }
688
689 if (lltok_isGt_Op (tok) )
690 {
691 return TRUE;
692 }
693 if (lltok_isLt_Op (tok) )
694 {
695 return TRUE;
696 }
697
698 if (lltok_isLe_Op (tok) )
699 {
700 return TRUE;
701 }
702
703 if (lltok_isGe_Op (tok) )
704 {
705 return TRUE;
706 }
707
708 return FALSE;
709
710}
711
712
713void exprNode_booleanTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint)
714{
715 constraint cons;
716exprNode t1, t2;
717exprData data;
718lltok tok;
719constraintList tempList;
720data = e->edata;
721
722tok = exprData_getOpTok (data);
723
724
725t1 = exprData_getOpA (data);
726t2 = exprData_getOpB (data);
727
728
729/* arithmetic tests */
730
731if (lltok_isEq_Op (tok) )
732{
733 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
734 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
735}
736
737
738 if (lltok_isLt_Op (tok) )
739 {
740 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
741 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
742 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
743 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
744 }
745
746
747if (lltok_isGe_Op (tok) )
748{
749
750 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
751 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
752
753 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
754 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
755
756}
757
758
759 if (lltok_isGt_Op (tok) )
760{
761 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
762 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
763 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
764 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
765}
766
767if (lltok_isLe_Op (tok) )
768{
769 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
770 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
771
772 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
773 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
774}
775
776
777
778/*Logical operations */
779
780 if (lltok_isAnd_Op (tok) )
781
782 {
783 //true ensures
784 tempList = constraintList_copy (t1->trueEnsuresConstraints);
785 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
786 e->trueEnsuresConstraints = constraintList_addList(e->trueEnsuresConstraints, tempList);
787
788 //false ensures: fens t1 or tens t1 and fens t2
789 tempList = constraintList_copy (t1->trueEnsuresConstraints);
790 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
791 tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
792 e->falseEnsuresConstraints =constraintList_addList(e->falseEnsuresConstraints, tempList);
793
794 }
795
796 if (lltok_isOr_Op (tok) )
797 {
798 //false ensures
799 tempList = constraintList_copy (t1->falseEnsuresConstraints);
800 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
801 e->falseEnsuresConstraints = constraintList_addList(e->falseEnsuresConstraints, tempList);
802
803 //true ensures: tens t1 or fens t1 and tens t2
804 tempList = constraintList_copy (t1->falseEnsuresConstraints);
805 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
806 tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
807 e->trueEnsuresConstraints =constraintList_addList(e->trueEnsuresConstraints, tempList);
808
809 }
810
811}
812
813bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint)
814{
9280addf 815 exprNode t1, t2, fcn;
616915dd 816 lltok tok;
817 bool handledExprNode;
818 exprData data;
819 constraint cons;
820
470b7798 821 if (exprNode_isError(e) )
822 {
823 return FALSE;
824 }
825
826 DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
616915dd 827 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
470b7798 828
c3e695ff 829 e->requiresConstraints = constraintList_makeNew();
830 e->ensuresConstraints = constraintList_makeNew();
831 e->trueEnsuresConstraints = constraintList_makeNew();;
832 e->falseEnsuresConstraints = constraintList_makeNew();;
470b7798 833
834 if (exprNode_isUnhandled (e) )
616915dd 835 {
836 return FALSE;
837 }
838 // e = makeDataTypeConstraints (e);
839
840 handledExprNode = TRUE;
841
842 data = e->edata;
843
844 switch (e->kind)
845 {
846
847
848 case XPR_WHILEPRED:
849 t1 = exprData_getSingle (data);
850 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
851 e = exprNode_copyConstraints (e, t1);
852 break;
853
854 case XPR_FETCH:
855
856 if (definatelv )
857 {
858 t1 = (exprData_getPairA (data) );
859 t2 = (exprData_getPairB (data) );
860 cons = constraint_makeWriteSafeExprNode (t1, t2);
861 }
862 else
863 {
864 t1 = (exprData_getPairA (data) );
865 t2 = (exprData_getPairB (data) );
866 cons = constraint_makeReadSafeExprNode (t1, t2 );
867 }
868
869 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
870 cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
871 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
872
9280addf 873 cons = constraint_makeEnsureLteMaxRead (t2, t1);
616915dd 874 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
875
876 // cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
877 // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
878
879 exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
880 exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
881
882 /*@i325 Should check which is array/index. */
883 break;
884
885 case XPR_PARENS:
886 exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
887 // e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
888 break;
889 case XPR_INIT:
890 /* //t1 = exprData_getInitId (data); */
891 t2 = exprData_getInitNode (data);
892 //exprNode_exprTraverse (t1, TRUE, FALSE, sequencePoint );
893
894 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
895
896 /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
897 if ( (!exprNode_isError (e)) && (!exprNode_isError(t2)) )
898 {
899 cons = constraint_makeEnsureEqual (e, t2, sequencePoint);
900 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
901 }
902
903 break;
904 case XPR_ASSIGN:
905 t1 = exprData_getOpA (data);
906 t2 = exprData_getOpB (data);
907 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
908 lltok_unparse (exprData_getOpTok (data));
909 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
910
911 /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
912 if ( (!exprNode_isError (t1)) && (!exprNode_isError(t2)) )
913 {
914 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
915 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
916 }
917 break;
918 case XPR_OP:
919 t1 = exprData_getOpA (data);
920 t2 = exprData_getOpB (data);
921
922 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
923 tok = exprData_getOpTok (data);
924 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
925
926 if (lltok_isBoolean_Op (tok) )
927 exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
928
929 // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
930 break;
931 case XPR_SIZEOFT:
932 ctype_unparse (qtype_getType (exprData_getType (data) ) );
933
934 break;
935
936 case XPR_SIZEOF:
937 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
938 // e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
939 break;
940
941 case XPR_CALL:
9280addf 942 fcn = exprData_getFcn(data);
943
944 exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint );
616915dd 945 exprNodeList_unparse (exprData_getArgs (data) );
9280addf 946 DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data) ) ) ) );
616915dd 947
9280addf 948 fcn->requiresConstraints = constraintList_addList (fcn->requiresConstraints,
949 checkCall (fcn, exprData_getArgs (data) ) );
616915dd 950
9280addf 951 fcn->ensuresConstraints = constraintList_addList (fcn->ensuresConstraints,
952 getPostConditions(fcn, exprData_getArgs (data),e ) );
953
954 t1 = exprNode_createNew (exprNode_getType (e) );
955
956 checkArgumentList (t1, exprData_getArgs(data), sequencePoint);
616915dd 957
9280addf 958
959 mergeResolve (e, t1, fcn);
960
616915dd 961 // e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) );
962 break;
963
964 case XPR_RETURN:
965 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
966 break;
967
968 case XPR_NULLRETURN:
969 cstring_makeLiteral ("return");;
970 break;
971
972
973 case XPR_FACCESS:
974 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
975 exprData_getFieldName (data) ;
976 break;
977
978 case XPR_ARROW:
979 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
980 exprData_getFieldName (data);
981 break;
982
983 case XPR_STRINGLITERAL:
984 cstring_copy (exprData_getLiteral (data));
985 break;
986
987 case XPR_NUMLIT:
988 cstring_copy (exprData_getLiteral (data));
989 break;
990
991 case XPR_PREOP:
992 t1 = exprData_getUopNode(data);
993 tok = (exprData_getUopTok (data));
994 //lltok_unparse (exprData_getUopTok (data));
995 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
996 /*handle * pointer access */
997 if (lltok_isInc_Op (tok) )
998 {
999 DPRINTF(("doing ++(var)"));
1000 t1 = exprData_getUopNode (data);
1001 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
1002 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1003 }
1004 else if (lltok_isDec_Op (tok) )
1005 {
1006 DPRINTF(("doing --(var)"));
1007 t1 = exprData_getUopNode (data);
1008 cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1009 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1010 }
1011
1012 if (lltok_isMult( exprData_getUopTok (data) ) )
1013 {
1014 if (definatelv)
1015 {
1016 cons = constraint_makeWriteSafeInt (t1, 0);
1017 }
1018 else
1019 {
1020 cons = constraint_makeReadSafeInt (t1, 0);
1021 }
1022 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1023 }
1024
1025 /* ! expr */
1026 if (lltok_isNot_Op (exprData_getUopTok (data) ) )
1027 {
1028 e->trueEnsuresConstraints = constraintList_copy (t1->falseEnsuresConstraints);
1029 e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
1030 }
1031 break;
1032
1033 case XPR_POSTOP:
1034
1035 exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
1036 lltok_unparse (exprData_getUopTok (data));
1037 if (lltok_isInc_Op (exprData_getUopTok (data) ) )
1038 {
1039 DPRINTF(("doing ++"));
1040 t1 = exprData_getUopNode (data);
1041 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
1042 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1043 }
1044 if (lltok_isDec_Op (exprData_getUopTok (data) ) )
1045 {
1046 DPRINTF(("doing --"));
1047 t1 = exprData_getUopNode (data);
1048 cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1049 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1050 }
1051 break;
470b7798 1052 case XPR_CAST:
1053 llassert(FALSE);
1054 exprNode_exprTraverse (exprData_getCastNode (data), definatelv, definaterv, sequencePoint );
1055 break;
1056 case XPR_COND:
1057 {
1058 exprNode pred, true, false;
1059 llassert(FALSE);
1060 pred = exprData_getTriplePred (data);
1061 true = exprData_getTripleTrue (data);
1062 false = exprData_getTripleFalse (data);
1063
1064 exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint );
1065 pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
1066 pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
1067
1068 pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred);
1069 pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
1070
1071 exprNode_exprTraverse (true, FALSE, TRUE, sequencePoint );
1072 true->ensuresConstraints = exprNode_traversEnsuresConstraints(true);
1073 true->requiresConstraints = exprNode_traversRequiresConstraints(true);
1074
1075 true->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(true);
1076 true->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(true);
1077
1078 exprNode_exprTraverse (false, FALSE, TRUE, sequencePoint );
1079 false->ensuresConstraints = exprNode_traversEnsuresConstraints(false);
1080 false->requiresConstraints = exprNode_traversRequiresConstraints(false);
1081
1082 false->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(false);
1083 false->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(false);
1084
1085
1086 /* if pred is true e equals true otherwise pred equals false */
1087
1088 cons = constraint_makeEnsureEqual (e, true, sequencePoint);
1089 true->ensuresConstraints = constraintList_add(true->ensuresConstraints, cons);
1090
1091 cons = constraint_makeEnsureEqual (e, true, sequencePoint);
1092 false->ensuresConstraints = constraintList_add(false->ensuresConstraints, cons);
1093
1094 e = doIfElse (e, pred, true, false);
1095
1096 }
1097 break;
1098 case XPR_COMMA:
1099 llassert(FALSE);
1100 t1 = exprData_getPairA (data);
1101 t2 = exprData_getPairB (data);
1102 /* we essiantially treat this like expr1; expr2
1103 of course sequencePoint isn't adjusted so this isn't completely accurate
1104 problems../ */
1105 exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint );
1106 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1107 mergeResolve (e, t1, t2);
1108 break;
1109
616915dd 1110 default:
1111 handledExprNode = FALSE;
1112 }
1113
1114 e->requiresConstraints = constraintList_preserveOrig ( e->requiresConstraints);
1115 e->ensuresConstraints = constraintList_preserveOrig ( e->ensuresConstraints);
9280addf 1116 e->requiresConstraints = constraintList_addGeneratingExpr ( e->requiresConstraints, e);
1117
1118 e->ensuresConstraints = constraintList_addGeneratingExpr ( e->ensuresConstraints, e);
1119
1120 DPRINTF((message ("ensures constraint for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
616915dd 1121
1122 return handledExprNode;
1123}
1124
1125
1126constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
1127{
470b7798 1128 exprNode t1;
616915dd 1129
1130 bool handledExprNode;
1131 // char * mes;
1132 exprData data;
1133 constraintList ret;
1134
1135 if (exprNode_handleError (e))
1136 {
c3e695ff 1137 ret = constraintList_makeNew();
616915dd 1138 return ret;
1139 }
1140 ret = constraintList_copy (e->trueEnsuresConstraints );
1141
1142 handledExprNode = TRUE;
1143
1144 data = e->edata;
1145
1146 switch (e->kind)
1147 {
9280addf 1148 case XPR_WHILEPRED:
1149 t1 = exprData_getSingle (data);
1150 ret = constraintList_addList ( ret,exprNode_traversTrueEnsuresConstraints (t1) );
1151 break;
616915dd 1152
1153 case XPR_FETCH:
1154
1155 ret = constraintList_addList (ret,
1156 exprNode_traversTrueEnsuresConstraints
1157 (exprData_getPairA (data) ) );
1158
1159 ret = constraintList_addList (ret,
1160 exprNode_traversTrueEnsuresConstraints
1161 (exprData_getPairB (data) ) );
1162 break;
1163 case XPR_PREOP:
1164
1165 ret = constraintList_addList (ret,
1166 exprNode_traversTrueEnsuresConstraints
1167 (exprData_getUopNode (data) ) );
1168 break;
1169
1170 case XPR_PARENS:
1171 ret = constraintList_addList (ret, exprNode_traversTrueEnsuresConstraints
1172 (exprData_getUopNode (data) ) );
1173 break;
1174 case XPR_ASSIGN:
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_OP:
1184 ret = constraintList_addList (ret,
1185 exprNode_traversTrueEnsuresConstraints
1186 (exprData_getOpA (data) ) );
1187
1188 ret = constraintList_addList (ret,
1189 exprNode_traversTrueEnsuresConstraints
1190 (exprData_getOpB (data) ) );
1191 break;
1192 case XPR_SIZEOFT:
1193
1194 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1195
1196 break;
1197
1198 case XPR_SIZEOF:
1199
1200 ret = constraintList_addList (ret,
1201 exprNode_traversTrueEnsuresConstraints
1202 (exprData_getSingle (data) ) );
1203 break;
1204
1205 case XPR_CALL:
1206 ret = constraintList_addList (ret,
1207 exprNode_traversTrueEnsuresConstraints
1208 (exprData_getFcn (data) ) );
1209 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1210 break;
1211
1212 case XPR_RETURN:
1213 ret = constraintList_addList (ret,
1214 exprNode_traversTrueEnsuresConstraints
1215 (exprData_getSingle (data) ) );
1216 break;
1217
1218 case XPR_NULLRETURN:
1219 // cstring_makeLiteral ("return");;
1220 break;
1221
1222 case XPR_FACCESS:
1223 ret = constraintList_addList (ret,
1224 exprNode_traversTrueEnsuresConstraints
1225 (exprData_getFieldNode (data) ) );
1226 //exprData_getFieldName (data) ;
1227 break;
1228
1229 case XPR_ARROW:
1230 ret = constraintList_addList (ret,
1231 exprNode_traversTrueEnsuresConstraints
1232 (exprData_getFieldNode (data) ) );
1233 // exprData_getFieldName (data);
1234 break;
1235
1236 case XPR_STRINGLITERAL:
1237 // cstring_copy (exprData_getLiteral (data));
1238 break;
1239
1240 case XPR_NUMLIT:
1241 // cstring_copy (exprData_getLiteral (data));
1242 break;
1243 case XPR_POSTOP:
1244
1245 ret = constraintList_addList (ret,
1246 exprNode_traversTrueEnsuresConstraints
1247 (exprData_getUopNode (data) ) );
1248 break;
470b7798 1249
1250 case XPR_CAST:
1251
1252 ret = constraintList_addList (ret,
1253 exprNode_traversTrueEnsuresConstraints
1254 (exprData_getCastNode (data) ) );
1255 break;
1256
1257 break;
616915dd 1258 default:
1259 break;
1260 }
1261
1262 return ret;
1263}
1264
9280addf 1265constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
1266{
470b7798 1267 exprNode t1;
9280addf 1268
1269 bool handledExprNode;
1270 // char * mes;
1271 exprData data;
1272 constraintList ret;
1273
1274 if (exprNode_handleError (e))
1275 {
c3e695ff 1276 ret = constraintList_makeNew();
9280addf 1277 return ret;
1278 }
1279 ret = constraintList_copy (e->falseEnsuresConstraints );
1280
1281 handledExprNode = TRUE;
1282
1283 data = e->edata;
1284
1285 switch (e->kind)
1286 {
1287 case XPR_WHILEPRED:
1288 t1 = exprData_getSingle (data);
1289 ret = constraintList_addList ( ret,exprNode_traversFalseEnsuresConstraints (t1) );
1290 break;
1291
1292 case XPR_FETCH:
1293
1294 ret = constraintList_addList (ret,
1295 exprNode_traversFalseEnsuresConstraints
1296 (exprData_getPairA (data) ) );
1297
1298 ret = constraintList_addList (ret,
1299 exprNode_traversFalseEnsuresConstraints
1300 (exprData_getPairB (data) ) );
1301 break;
1302 case XPR_PREOP:
1303
1304 ret = constraintList_addList (ret,
1305 exprNode_traversFalseEnsuresConstraints
1306 (exprData_getUopNode (data) ) );
1307 break;
1308
1309 case XPR_PARENS:
1310 ret = constraintList_addList (ret, exprNode_traversFalseEnsuresConstraints
1311 (exprData_getUopNode (data) ) );
1312 break;
1313 case XPR_ASSIGN:
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_OP:
1323 ret = constraintList_addList (ret,
1324 exprNode_traversFalseEnsuresConstraints
1325 (exprData_getOpA (data) ) );
1326
1327 ret = constraintList_addList (ret,
1328 exprNode_traversFalseEnsuresConstraints
1329 (exprData_getOpB (data) ) );
1330 break;
1331 case XPR_SIZEOFT:
1332
1333 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1334
1335 break;
1336
1337 case XPR_SIZEOF:
1338
1339 ret = constraintList_addList (ret,
1340 exprNode_traversFalseEnsuresConstraints
1341 (exprData_getSingle (data) ) );
1342 break;
1343
1344 case XPR_CALL:
1345 ret = constraintList_addList (ret,
1346 exprNode_traversFalseEnsuresConstraints
1347 (exprData_getFcn (data) ) );
1348 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1349 break;
1350
1351 case XPR_RETURN:
1352 ret = constraintList_addList (ret,
1353 exprNode_traversFalseEnsuresConstraints
1354 (exprData_getSingle (data) ) );
1355 break;
1356
1357 case XPR_NULLRETURN:
1358 // cstring_makeLiteral ("return");;
1359 break;
1360
1361 case XPR_FACCESS:
1362 ret = constraintList_addList (ret,
1363 exprNode_traversFalseEnsuresConstraints
1364 (exprData_getFieldNode (data) ) );
1365 //exprData_getFieldName (data) ;
1366 break;
1367
1368 case XPR_ARROW:
1369 ret = constraintList_addList (ret,
1370 exprNode_traversFalseEnsuresConstraints
1371 (exprData_getFieldNode (data) ) );
1372 // exprData_getFieldName (data);
1373 break;
1374
1375 case XPR_STRINGLITERAL:
1376 // cstring_copy (exprData_getLiteral (data));
1377 break;
1378
1379 case XPR_NUMLIT:
1380 // cstring_copy (exprData_getLiteral (data));
1381 break;
1382 case XPR_POSTOP:
1383
1384 ret = constraintList_addList (ret,
1385 exprNode_traversFalseEnsuresConstraints
1386 (exprData_getUopNode (data) ) );
1387 break;
470b7798 1388
1389 case XPR_CAST:
1390
1391 ret = constraintList_addList (ret,
1392 exprNode_traversFalseEnsuresConstraints
1393 (exprData_getCastNode (data) ) );
1394 break;
1395
9280addf 1396 default:
1397 break;
1398 }
1399
1400 return ret;
1401}
1402
616915dd 1403
1404/* walk down the tree and get all requires Constraints in each subexpression*/
1405constraintList exprNode_traversRequiresConstraints (exprNode e)
1406{
470b7798 1407 exprNode t1;
616915dd 1408
1409 bool handledExprNode;
1410 // char * mes;
1411 exprData data;
1412 constraintList ret;
1413
1414 if (exprNode_handleError (e))
1415 {
c3e695ff 1416 ret = constraintList_makeNew();
616915dd 1417 return ret;
1418 }
1419 ret = constraintList_copy (e->requiresConstraints );
1420
1421 handledExprNode = TRUE;
1422
1423 data = e->edata;
1424
1425 switch (e->kind)
1426 {
9280addf 1427 case XPR_WHILEPRED:
1428 t1 = exprData_getSingle (data);
1429 ret = constraintList_addList ( ret,exprNode_traversRequiresConstraints (t1) );
1430 break;
616915dd 1431
1432 case XPR_FETCH:
1433
1434 ret = constraintList_addList (ret,
1435 exprNode_traversRequiresConstraints
1436 (exprData_getPairA (data) ) );
1437
1438 ret = constraintList_addList (ret,
1439 exprNode_traversRequiresConstraints
1440 (exprData_getPairB (data) ) );
1441 break;
1442 case XPR_PREOP:
1443
1444 ret = constraintList_addList (ret,
1445 exprNode_traversRequiresConstraints
1446 (exprData_getUopNode (data) ) );
1447 break;
1448
1449 case XPR_PARENS:
1450 ret = constraintList_addList (ret, exprNode_traversRequiresConstraints
1451 (exprData_getUopNode (data) ) );
1452 break;
1453 case XPR_ASSIGN:
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_OP:
1463 ret = constraintList_addList (ret,
1464 exprNode_traversRequiresConstraints
1465 (exprData_getOpA (data) ) );
1466
1467 ret = constraintList_addList (ret,
1468 exprNode_traversRequiresConstraints
1469 (exprData_getOpB (data) ) );
1470 break;
1471 case XPR_SIZEOFT:
1472
1473 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1474
1475 break;
1476
1477 case XPR_SIZEOF:
1478
1479 ret = constraintList_addList (ret,
1480 exprNode_traversRequiresConstraints
1481 (exprData_getSingle (data) ) );
1482 break;
1483
1484 case XPR_CALL:
1485 ret = constraintList_addList (ret,
1486 exprNode_traversRequiresConstraints
1487 (exprData_getFcn (data) ) );
1488 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1489 break;
1490
1491 case XPR_RETURN:
1492 ret = constraintList_addList (ret,
1493 exprNode_traversRequiresConstraints
1494 (exprData_getSingle (data) ) );
1495 break;
1496
1497 case XPR_NULLRETURN:
1498 // cstring_makeLiteral ("return");;
1499 break;
1500
1501 case XPR_FACCESS:
1502 ret = constraintList_addList (ret,
1503 exprNode_traversRequiresConstraints
1504 (exprData_getFieldNode (data) ) );
1505 //exprData_getFieldName (data) ;
1506 break;
1507
1508 case XPR_ARROW:
1509 ret = constraintList_addList (ret,
1510 exprNode_traversRequiresConstraints
1511 (exprData_getFieldNode (data) ) );
1512 // exprData_getFieldName (data);
1513 break;
1514
1515 case XPR_STRINGLITERAL:
1516 // cstring_copy (exprData_getLiteral (data));
1517 break;
1518
1519 case XPR_NUMLIT:
1520 // cstring_copy (exprData_getLiteral (data));
1521 break;
1522 case XPR_POSTOP:
1523
1524 ret = constraintList_addList (ret,
1525 exprNode_traversRequiresConstraints
1526 (exprData_getUopNode (data) ) );
1527 break;
470b7798 1528
1529 case XPR_CAST:
1530
1531 ret = constraintList_addList (ret,
1532 exprNode_traversRequiresConstraints
1533 (exprData_getCastNode (data) ) );
1534 break;
1535
616915dd 1536 default:
1537 break;
1538 }
1539
1540 return ret;
1541}
1542
1543
1544/* walk down the tree and get all Ensures Constraints in each subexpression*/
1545constraintList exprNode_traversEnsuresConstraints (exprNode e)
1546{
470b7798 1547 exprNode t1;
616915dd 1548
1549 bool handledExprNode;
1550 // char * mes;
1551 exprData data;
1552 // constraintExpr tmp;
1553 // constraint cons;
1554 constraintList ret;
1555
1556
1557 if (exprNode_handleError (e))
1558 {
c3e695ff 1559 ret = constraintList_makeNew();
616915dd 1560 return ret;
1561 }
1562
1563 ret = constraintList_copy (e->ensuresConstraints );
1564 handledExprNode = TRUE;
1565
1566 data = e->edata;
1567
1568 DPRINTF( (message (
1569 "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
1570 exprNode_unparse (e),
1571 constraintList_print(e->ensuresConstraints)
1572 )
1573 ));
1574
1575
1576 switch (e->kind)
1577 {
9280addf 1578 case XPR_WHILEPRED:
1579 t1 = exprData_getSingle (data);
1580 ret = constraintList_addList ( ret,exprNode_traversEnsuresConstraints (t1) );
1581 break;
616915dd 1582
1583 case XPR_FETCH:
1584
1585 ret = constraintList_addList (ret,
1586 exprNode_traversEnsuresConstraints
1587 (exprData_getPairA (data) ) );
1588
1589 ret = constraintList_addList (ret,
1590 exprNode_traversEnsuresConstraints
1591 (exprData_getPairB (data) ) );
1592 break;
1593 case XPR_PREOP:
1594
1595 ret = constraintList_addList (ret,
1596 exprNode_traversEnsuresConstraints
1597 (exprData_getUopNode (data) ) );
1598 break;
1599
1600 case XPR_PARENS:
1601 ret = constraintList_addList (ret, exprNode_traversEnsuresConstraints
1602 (exprData_getUopNode (data) ) );
1603 break;
1604 case XPR_ASSIGN:
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_OP:
1614 ret = constraintList_addList (ret,
1615 exprNode_traversEnsuresConstraints
1616 (exprData_getOpA (data) ) );
1617
1618 ret = constraintList_addList (ret,
1619 exprNode_traversEnsuresConstraints
1620 (exprData_getOpB (data) ) );
1621 break;
1622 case XPR_SIZEOFT:
1623
1624 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1625
1626 break;
1627
1628 case XPR_SIZEOF:
1629
1630 ret = constraintList_addList (ret,
1631 exprNode_traversEnsuresConstraints
1632 (exprData_getSingle (data) ) );
1633 break;
1634
1635 case XPR_CALL:
1636 ret = constraintList_addList (ret,
1637 exprNode_traversEnsuresConstraints
1638 (exprData_getFcn (data) ) );
1639 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1640 break;
1641
1642 case XPR_RETURN:
1643 ret = constraintList_addList (ret,
1644 exprNode_traversEnsuresConstraints
1645 (exprData_getSingle (data) ) );
1646 break;
1647
1648 case XPR_NULLRETURN:
1649 // cstring_makeLiteral ("return");;
1650 break;
1651
1652 case XPR_FACCESS:
1653 ret = constraintList_addList (ret,
1654 exprNode_traversEnsuresConstraints
1655 (exprData_getFieldNode (data) ) );
1656 //exprData_getFieldName (data) ;
1657 break;
1658
1659 case XPR_ARROW:
1660 ret = constraintList_addList (ret,
1661 exprNode_traversEnsuresConstraints
1662 (exprData_getFieldNode (data) ) );
1663 // exprData_getFieldName (data);
1664 break;
1665
1666 case XPR_STRINGLITERAL:
1667 // cstring_copy (exprData_getLiteral (data));
1668 break;
1669
1670 case XPR_NUMLIT:
1671 // cstring_copy (exprData_getLiteral (data));
1672 break;
1673 case XPR_POSTOP:
1674
1675 ret = constraintList_addList (ret,
1676 exprNode_traversEnsuresConstraints
1677 (exprData_getUopNode (data) ) );
1678 break;
470b7798 1679 case XPR_CAST:
1680
1681 ret = constraintList_addList (ret,
1682 exprNode_traversEnsuresConstraints
1683 (exprData_getCastNode (data) ) );
1684 break;
1685
616915dd 1686 default:
1687 break;
1688 }
1689DPRINTF( (message (
1690 "exprnode_traversEnsuresConstraints call for %s with constraintList of is returning %s",
1691 exprNode_unparse (e),
1692 // constraintList_print(e->ensuresConstraints),
1693 constraintList_print(ret)
1694 )
1695 ));
1696
1697
1698 return ret;
1699}
1700
git-cvsimport mirror of splint
This page took 0.304712 seconds and 5 git commands to generate.