]> andersk Git - splint.git/blame - src/constraintGeneration.c
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Converted to new API for constraintExpr
[splint.git] / src / constraintGeneration.c
CommitLineData
4cccc6ad 1
2/*
3** constraintList.c
4*/
5
6# include <ctype.h> /* for isdigit */
7# include "lclintMacros.nf"
8# include "basic.h"
9# include "cgrammar.h"
10# include "cgrammar_tokens.h"
11
12# include "exprChecks.h"
13# include "aliasChecks.h"
14# include "exprNodeSList.h"
15# include "exprData.i"
16
17void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e);
18static bool exprNode_handleError( exprNode p_e);
19
361091cc 20//static cstring exprNode_findConstraints ( exprNode p_e);
4cccc6ad 21static bool exprNode_isMultiStatement(exprNode p_e);
22static bool exprNode_multiStatement (exprNode p_e);
23bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint);
361091cc 24//static void exprNode_constraintPropagateUp (exprNode p_e);
25constraintList exprNode_traversRequiresConstraints (exprNode e);
26constraintList exprNode_traversEnsuresConstraints (exprNode e);
27void mergeResolve (exprNode parent, exprNode child1, exprNode child2);
4cccc6ad 28
29
361091cc 30
4cccc6ad 31bool exprNode_isUnhandled (exprNode e)
32{
33 llassert( exprNode_isDefined(e) );
34 switch (e->kind)
35 {
36 case XPR_INITBLOCK:
37 case XPR_EMPTY:
38 case XPR_LABEL:
39 case XPR_CONST:
40 case XPR_VAR:
41 case XPR_BODY:
42 case XPR_OFFSETOF:
43 case XPR_ALIGNOFT:
44 case XPR_ALIGNOF:
45 case XPR_VAARG:
46 case XPR_ITERCALL:
47 case XPR_ITER:
48 case XPR_CAST:
49 case XPR_GOTO:
50 case XPR_CONTINUE:
51 case XPR_BREAK:
52 case XPR_COMMA:
53 case XPR_COND:
54 case XPR_TOK:
55 case XPR_FTDEFAULT:
56 case XPR_DEFAULT:
57 case XPR_SWITCH:
58 case XPR_FTCASE:
59 case XPR_CASE:
60 case XPR_INIT:
61 case XPR_NODE:
62 DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) );
63 return FALSE;
64 /*@notreached@*/
65 break;
66 default:
67 return TRUE;
68
69 }
70 /*not reached*/
71 return FALSE;
72}
73
74bool exprNode_handleError( exprNode e)
75{
76 if (exprNode_isError (e) || !exprNode_isUnhandled(e) )
77 {
78 static /*@only@*/ cstring error = cstring_undefined;
79
80 if (!cstring_isDefined (error))
81 {
82 error = cstring_makeLiteral ("<error>");
83 }
84
85 /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/
86 }
87 return FALSE;
88}
89
90void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e)
91{
92 DPRINTF((message ("exprNode_gnerateConstraints Analysising %s %s at", exprNode_unparse( e),
93 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
94
95 if (exprNode_isMultiStatement ( e) )
96 {
bf92e32c 97 exprNode_multiStatement(e);
4cccc6ad 98 }
99 else
100 {
101 llassert(FALSE);
102 }
bf92e32c 103 printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) );
104 printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) );
4cccc6ad 105 return FALSE;
106}
107
108
109/* handles multiple statements */
110
111bool exprNode_isMultiStatement(exprNode e)
112{
113if (exprNode_handleError (e) != NULL)
114 return FALSE;
115
116 switch (e->kind)
117 {
118 case XPR_FOR:
119 case XPR_FORPRED:
120 case XPR_IF:
121 case XPR_IFELSE:
122 case XPR_WHILE:
123 case XPR_WHILEPRED:
124 case XPR_DOWHILE:
125 case XPR_BLOCK:
126 case XPR_STMT:
127 case XPR_STMTLIST:
128 return TRUE;
129 default:
130 return FALSE;
131 }
132
133}
134
135bool exprNode_stmt (exprNode e)
136{
137 exprNode snode;
361091cc 138 fileloc loc;
139 bool notError;
4cccc6ad 140
141 if (exprNode_isError(e) )
142 {
143 return FALSE;
144 }
361091cc 145 e->requiresConstraints = constraintList_new();
146 e->ensuresConstraints = constraintList_new();
4cccc6ad 147
361091cc 148
149 DPRINTF(( "STMT:") );
150 DPRINTF ( ( cstring_toCharsSafe ( exprNode_unparse(e)) )
4cccc6ad 151 );
152 if (e->kind != XPR_STMT)
153 {
154
361091cc 155 DPRINTF (("Not Stmt") );
156 DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
4cccc6ad 157 if (exprNode_isMultiStatement (e) )
158 {
159 return exprNode_multiStatement (e );
160 }
161 llassert(FALSE);
162 }
361091cc 163
164 DPRINTF (("Stmt") );
165 DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
166
4cccc6ad 167 snode = exprData_getUopNode (e->edata);
168
169 /* could be stmt involving multiple statements:
170 i.e. if, while for ect.
171 */
172
173 if (exprNode_isMultiStatement (snode))
174 {
175 llassert(FALSE);
176 return exprNode_multiStatement (snode);
177 }
361091cc 178
179 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
180 notError = exprNode_exprTraverse (snode, FALSE, FALSE, loc);
181 e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
92c4a786 182 printf ("For: %s \n", exprNode_unparse (e) );
183 printf ("%s\n", constraintList_print(e->requiresConstraints) );
361091cc 184 e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode);
92c4a786 185 printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
361091cc 186 llassert(notError);
187 return notError;
188
4cccc6ad 189}
190
191
192bool exprNode_stmtList (exprNode e)
193{
361091cc 194 exprNode stmt1, stmt2;
4cccc6ad 195 if (exprNode_isError (e) )
196 {
197 return FALSE;
198 }
361091cc 199
200 e->requiresConstraints = constraintList_new();
201 e->ensuresConstraints = constraintList_new();
202
4cccc6ad 203 /*Handle case of stmtList with only one statement:
204 The parse tree stores this as stmt instead of stmtList*/
205 if (e->kind != XPR_STMTLIST)
206 {
207 return exprNode_stmt(e);
208 }
209 llassert (e->kind == XPR_STMTLIST);
361091cc 210 DPRINTF(( "STMTLIST:") );
211 DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
212 stmt1 = exprData_getPairA (e->edata);
213 stmt2 = exprData_getPairB (e->edata);
214
6364363c 215
216 DPRINTF(("XW stmtlist ") );
217 DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
218
361091cc 219 exprNode_stmt (stmt1);
220 DPRINTF(("\nstmt after stmtList call " ));
221
222 exprNode_stmt (stmt2);
361091cc 223 mergeResolve (e, stmt1, stmt2 );
92c4a786 224
bf92e32c 225 DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
361091cc 226 constraintList_print(e->requiresConstraints),
227 constraintList_print(e->ensuresConstraints) ) ) );
228 return TRUE;
4cccc6ad 229}
230
361091cc 231
4cccc6ad 232bool exprNode_multiStatement (exprNode e)
233{
234
235 bool ret;
236 exprData data;
237
238
239 DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
240 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
241
242 if (exprNode_handleError (e))
243 {
244 return FALSE;
245 }
246
247 data = e->edata;
248
249 ret = TRUE;
250
251 switch (e->kind)
252 {
253
254 case XPR_FOR:
255 // ret = message ("%s %s",
256 exprNode_generateConstraints (exprData_getPairA (data));
257 exprNode_generateConstraints (exprData_getPairB (data));
258 break;
259
260 case XPR_FORPRED:
261 // ret = message ("for (%s; %s; %s)",
262 exprNode_generateConstraints (exprData_getTripleInit (data));
263 exprNode_generateConstraints (exprData_getTripleTest (data));
264 exprNode_generateConstraints (exprData_getTripleInc (data));
265 break;
266 case XPR_IF:
361091cc 267 DPRINTF(( "IF:") );
268 DPRINTF ((exprNode_unparse(e) ) );
4cccc6ad 269 // ret = message ("if (%s) %s",
270 exprNode_generateConstraints (exprData_getPairA (data));
271 exprNode_generateConstraints (exprData_getPairB (data));
272 // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
273 break;
274
275 case XPR_IFELSE:
276 // ret = message ("if (%s) %s else %s",
277 exprNode_generateConstraints (exprData_getTriplePred (data));
278 exprNode_generateConstraints (exprData_getTripleTrue (data));
279 exprNode_generateConstraints (exprData_getTripleFalse (data));
280 break;
281 case XPR_WHILE:
282 // ret = message ("while (%s) %s",
283 exprNode_generateConstraints (exprData_getPairA (data));
284 exprNode_generateConstraints (exprData_getPairB (data));
285 // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), exprData_getPairB (data) );
286 break;
287
288 case XPR_WHILEPRED:
289 // ret =
290 // cstring_copy (
291 exprNode_generateConstraints (exprData_getSingle (data));
292 break;
293
294 case XPR_DOWHILE:
295 // ret = message ("do { %s } while (%s)",
296 exprNode_generateConstraints (exprData_getPairB (data));
297 exprNode_generateConstraints (exprData_getPairA (data));
298 break;
299
300 case XPR_BLOCK:
301 // ret = message ("{ %s }",
302 exprNode_generateConstraints (exprData_getSingle (data));
361091cc 303 e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
304 e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
305 // e->constraints = (exprData_getSingle (data))->constraints;
4cccc6ad 306 break;
307
308 case XPR_STMT:
309 case XPR_STMTLIST:
310 return exprNode_stmtList (e);
311 /*@notreached@*/
312 break;
313 default:
314 ret=FALSE;
315 }
316 return ret;
317}
318
319
4cccc6ad 320bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint)
321{
322 exprNode t1, t2;
323
324 bool handledExprNode;
4cccc6ad 325 exprData data;
4cccc6ad 326 constraint cons;
327
328 DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
329 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
361091cc 330
331 e->requiresConstraints = constraintList_new();
332 e->ensuresConstraints = constraintList_new();
4cccc6ad 333
334 if (exprNode_handleError (e))
335 {
336 return FALSE;
337 }
338
339 handledExprNode = TRUE;
340
341 data = e->edata;
342
343 switch (e->kind)
344 {
345
346 case XPR_FETCH:
347
4cccc6ad 348 if (definatelv )
349 {
350 t1 = (exprData_getPairA (data) );
351 t2 = (exprData_getPairB (data) );
361091cc 352 cons = constraint_makeWriteSafeExprNode (t1, t2);
4cccc6ad 353 }
354 else
355 {
356 t1 = (exprData_getPairA (data) );
357 t2 = (exprData_getPairB (data) );
361091cc 358 cons = constraint_makeReadSafeExprNode (t1, t2 );
4cccc6ad 359 }
361091cc 360
361 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
4cccc6ad 362 cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
361091cc 363 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
bf92e32c 364 // cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
365 // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
361091cc 366
4cccc6ad 367 exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
368 exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
369
370 /*@i325 Should check which is array/index. */
4cccc6ad 371 break;
372 case XPR_PREOP:
373 t1 = exprData_getUopNode(data);
374 lltok_unparse (exprData_getUopTok (data));
375 exprNode_exprTraverse (exprData_getUopNode (data), definatelv, definaterv, sequencePoint );
376 /*handle * pointer access */
377
378 /*@ i 325 do ++ and -- */
379 if (lltok_isMult( exprData_getUopTok (data) ) )
380 {
381 if (definatelv)
382 {
361091cc 383 cons = constraint_makeWriteSafeInt (t1, 0);
4cccc6ad 384 }
385 else
386 {
387 cons = constraint_makeReadSafeInt (t1, 0);
4cccc6ad 388 }
361091cc 389 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
390 }
391 if (lltok_isInc_Op (exprData_getUopTok (data) ) )
392 {
393 // cons = constraint_makeSideEffectPostIncrement (t1, sequencePoint);
394 // e->ensuresConstraints = constraintList_add(e->requiresConstraints, cons);
4cccc6ad 395 }
4cccc6ad 396 break;
397
398 case XPR_PARENS:
399 exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
361091cc 400 // e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
bf92e32c 401 break;
4cccc6ad 402 case XPR_ASSIGN:
403 exprNode_exprTraverse (exprData_getOpA (data), TRUE, definaterv, sequencePoint );
404 lltok_unparse (exprData_getOpTok (data));
405 exprNode_exprTraverse (exprData_getOpB (data), definatelv, TRUE, sequencePoint );
361091cc 406 // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data) );
4cccc6ad 407 break;
408 case XPR_OP:
409 exprNode_exprTraverse (exprData_getOpA (data), definatelv, definaterv, sequencePoint );
410 lltok_unparse (exprData_getOpTok (data));
411 exprNode_exprTraverse (exprData_getOpB (data), definatelv, definaterv, sequencePoint );
412
361091cc 413 // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
4cccc6ad 414 break;
415 case XPR_SIZEOFT:
416 ctype_unparse (qtype_getType (exprData_getType (data) ) );
417
418 break;
419
420 case XPR_SIZEOF:
421 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
361091cc 422 // e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
4cccc6ad 423 break;
424
425 case XPR_CALL:
426 exprNode_exprTraverse (exprData_getFcn (data), definatelv, definaterv, sequencePoint );
427 exprNodeList_unparse (exprData_getArgs (data) );
428 // e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) );
429 break;
430
431 case XPR_RETURN:
432 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
433 break;
434
435 case XPR_NULLRETURN:
436 cstring_makeLiteral ("return");;
437 break;
438
439
440 case XPR_FACCESS:
441 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
442 exprData_getFieldName (data) ;
443 break;
444
445 case XPR_ARROW:
446 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
447 exprData_getFieldName (data);
448 break;
449
450 case XPR_STRINGLITERAL:
451 cstring_copy (exprData_getLiteral (data));
452 break;
453
454 case XPR_NUMLIT:
455 cstring_copy (exprData_getLiteral (data));
456 break;
457 case XPR_POSTOP:
458
459 exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
460 lltok_unparse (exprData_getUopTok (data));
4cccc6ad 461 if (lltok_isInc_Op (exprData_getUopTok (data) ) )
462 {
bf92e32c 463 DPRINTF(("doing ++"));
4cccc6ad 464 t1 = exprData_getUopNode (data);
361091cc 465 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
466 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
bf92e32c 467 // cons = constraint_makeMaxReadSideEffectPostIncrement (t1, sequencePoint );
468 //e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
4cccc6ad 469 }
470 break;
471 default:
472 handledExprNode = FALSE;
473 }
474
bf92e32c 475 e->requiresConstraints = constraintList_preserveOrig ( e->requiresConstraints);
476 e->ensuresConstraints = constraintList_preserveOrig ( e->ensuresConstraints);
477
4cccc6ad 478 return handledExprNode;
479}
480
361091cc 481/* walk down the tree and get all requires Constraints in each subexpression*/
482constraintList exprNode_traversRequiresConstraints (exprNode e)
483{
484 // exprNode t1, t2;
485
486 bool handledExprNode;
487 // char * mes;
488 exprData data;
489 constraintList ret;
490 ret = constraintList_copy (e->requiresConstraints );
491 if (exprNode_handleError (e))
492 {
493 return ret;
494 }
495
496 handledExprNode = TRUE;
497
498 data = e->edata;
499
500 switch (e->kind)
501 {
502
503 case XPR_FETCH:
504
505 ret = constraintList_addList (ret,
506 exprNode_traversRequiresConstraints
507 (exprData_getPairA (data) ) );
508
509 ret = constraintList_addList (ret,
510 exprNode_traversRequiresConstraints
511 (exprData_getPairB (data) ) );
512 break;
513 case XPR_PREOP:
514
515 ret = constraintList_addList (ret,
516 exprNode_traversRequiresConstraints
517 (exprData_getUopNode (data) ) );
518 break;
519
520 case XPR_PARENS:
521 ret = constraintList_addList (ret, exprNode_traversRequiresConstraints
522 (exprData_getUopNode (data) ) );
523 break;
524 case XPR_ASSIGN:
525 ret = constraintList_addList (ret,
526 exprNode_traversRequiresConstraints
527 (exprData_getOpA (data) ) );
528
529 ret = constraintList_addList (ret,
530 exprNode_traversRequiresConstraints
531 (exprData_getOpB (data) ) );
532 break;
533 case XPR_OP:
534 ret = constraintList_addList (ret,
535 exprNode_traversRequiresConstraints
536 (exprData_getOpA (data) ) );
537
538 ret = constraintList_addList (ret,
539 exprNode_traversRequiresConstraints
540 (exprData_getOpB (data) ) );
541 break;
542 case XPR_SIZEOFT:
543
544 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
545
546 break;
547
548 case XPR_SIZEOF:
549
550 ret = constraintList_addList (ret,
551 exprNode_traversRequiresConstraints
552 (exprData_getSingle (data) ) );
553 break;
554
555 case XPR_CALL:
556 ret = constraintList_addList (ret,
557 exprNode_traversRequiresConstraints
558 (exprData_getFcn (data) ) );
559 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
560 break;
561
562 case XPR_RETURN:
563 ret = constraintList_addList (ret,
564 exprNode_traversRequiresConstraints
565 (exprData_getSingle (data) ) );
566 break;
567
568 case XPR_NULLRETURN:
569 // cstring_makeLiteral ("return");;
570 break;
571
572 case XPR_FACCESS:
573 ret = constraintList_addList (ret,
574 exprNode_traversRequiresConstraints
575 (exprData_getFieldNode (data) ) );
576 //exprData_getFieldName (data) ;
577 break;
578
579 case XPR_ARROW:
580 ret = constraintList_addList (ret,
581 exprNode_traversRequiresConstraints
582 (exprData_getFieldNode (data) ) );
583 // exprData_getFieldName (data);
584 break;
585
586 case XPR_STRINGLITERAL:
587 // cstring_copy (exprData_getLiteral (data));
588 break;
589
590 case XPR_NUMLIT:
591 // cstring_copy (exprData_getLiteral (data));
592 break;
593 case XPR_POSTOP:
594
595 ret = constraintList_addList (ret,
596 exprNode_traversRequiresConstraints
597 (exprData_getUopNode (data) ) );
598 break;
599 default:
600 break;
601 }
602
603 return ret;
604}
605
606
607/* walk down the tree and get all Ensures Constraints in each subexpression*/
608constraintList exprNode_traversEnsuresConstraints (exprNode e)
609{
610 // exprNode t1, t2;
611
612 bool handledExprNode;
613 // char * mes;
614 exprData data;
615 // constraintExpr tmp;
616 // constraint cons;
617 constraintList ret;
618 ret = constraintList_copy (e->ensuresConstraints );
619 if (exprNode_handleError (e))
620 {
621 return ret;
622 }
623
624 handledExprNode = TRUE;
625
626 data = e->edata;
627
628 DPRINTF( (message (
629 "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
630 exprNode_unparse (e),
631 constraintList_print(e->ensuresConstraints)
632 )
633 ));
634
635
636 switch (e->kind)
637 {
638
639 case XPR_FETCH:
640
641 ret = constraintList_addList (ret,
642 exprNode_traversEnsuresConstraints
643 (exprData_getPairA (data) ) );
644
645 ret = constraintList_addList (ret,
646 exprNode_traversEnsuresConstraints
647 (exprData_getPairB (data) ) );
648 break;
649 case XPR_PREOP:
650
651 ret = constraintList_addList (ret,
652 exprNode_traversEnsuresConstraints
653 (exprData_getUopNode (data) ) );
654 break;
655
656 case XPR_PARENS:
657 ret = constraintList_addList (ret, exprNode_traversEnsuresConstraints
658 (exprData_getUopNode (data) ) );
659 break;
660 case XPR_ASSIGN:
661 ret = constraintList_addList (ret,
662 exprNode_traversEnsuresConstraints
663 (exprData_getOpA (data) ) );
664
665 ret = constraintList_addList (ret,
666 exprNode_traversEnsuresConstraints
667 (exprData_getOpB (data) ) );
668 break;
669 case XPR_OP:
670 ret = constraintList_addList (ret,
671 exprNode_traversEnsuresConstraints
672 (exprData_getOpA (data) ) );
673
674 ret = constraintList_addList (ret,
675 exprNode_traversEnsuresConstraints
676 (exprData_getOpB (data) ) );
677 break;
678 case XPR_SIZEOFT:
679
680 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
681
682 break;
683
684 case XPR_SIZEOF:
685
686 ret = constraintList_addList (ret,
687 exprNode_traversEnsuresConstraints
688 (exprData_getSingle (data) ) );
689 break;
690
691 case XPR_CALL:
692 ret = constraintList_addList (ret,
693 exprNode_traversEnsuresConstraints
694 (exprData_getFcn (data) ) );
695 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
696 break;
697
698 case XPR_RETURN:
699 ret = constraintList_addList (ret,
700 exprNode_traversEnsuresConstraints
701 (exprData_getSingle (data) ) );
702 break;
703
704 case XPR_NULLRETURN:
705 // cstring_makeLiteral ("return");;
706 break;
707
708 case XPR_FACCESS:
709 ret = constraintList_addList (ret,
710 exprNode_traversEnsuresConstraints
711 (exprData_getFieldNode (data) ) );
712 //exprData_getFieldName (data) ;
713 break;
714
715 case XPR_ARROW:
716 ret = constraintList_addList (ret,
717 exprNode_traversEnsuresConstraints
718 (exprData_getFieldNode (data) ) );
719 // exprData_getFieldName (data);
720 break;
721
722 case XPR_STRINGLITERAL:
723 // cstring_copy (exprData_getLiteral (data));
724 break;
725
726 case XPR_NUMLIT:
727 // cstring_copy (exprData_getLiteral (data));
728 break;
729 case XPR_POSTOP:
730
731 ret = constraintList_addList (ret,
732 exprNode_traversEnsuresConstraints
733 (exprData_getUopNode (data) ) );
734 break;
735 default:
736 break;
737 }
738DPRINTF( (message (
739 "exprnode_traversEnsuresConstraints call for %s with constraintList of is returning %s",
740 exprNode_unparse (e),
741 // constraintList_print(e->ensuresConstraints),
742 constraintList_print(ret)
743 )
744 ));
745
746
747 return ret;
748}
749
git-cvsimport mirror of splint
This page took 0.160233 seconds and 5 git commands to generate.