]> andersk Git - splint.git/blame - src/constraintGeneration.c
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
It mostly works but it has a convolted API that needs fixxing.
[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);
bf92e32c 182 // printf ("%s\n", constraintList_print(e->requiresConstraints) );
361091cc 183 e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode);
bf92e32c 184 // printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
361091cc 185 llassert(notError);
186 return notError;
187
4cccc6ad 188}
189
190
191bool exprNode_stmtList (exprNode e)
192{
361091cc 193 exprNode stmt1, stmt2;
4cccc6ad 194 if (exprNode_isError (e) )
195 {
196 return FALSE;
197 }
361091cc 198
199 e->requiresConstraints = constraintList_new();
200 e->ensuresConstraints = constraintList_new();
201
4cccc6ad 202 /*Handle case of stmtList with only one statement:
203 The parse tree stores this as stmt instead of stmtList*/
204 if (e->kind != XPR_STMTLIST)
205 {
206 return exprNode_stmt(e);
207 }
208 llassert (e->kind == XPR_STMTLIST);
361091cc 209 DPRINTF(( "STMTLIST:") );
210 DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
211 stmt1 = exprData_getPairA (e->edata);
212 stmt2 = exprData_getPairB (e->edata);
213
6364363c 214
215 DPRINTF(("XW stmtlist ") );
216 DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
217
361091cc 218 exprNode_stmt (stmt1);
219 DPRINTF(("\nstmt after stmtList call " ));
220
221 exprNode_stmt (stmt2);
361091cc 222 mergeResolve (e, stmt1, stmt2 );
bf92e32c 223 DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
361091cc 224 constraintList_print(e->requiresConstraints),
225 constraintList_print(e->ensuresConstraints) ) ) );
226 return TRUE;
4cccc6ad 227}
228
361091cc 229
4cccc6ad 230bool exprNode_multiStatement (exprNode e)
231{
232
233 bool ret;
234 exprData data;
235
236
237 DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
238 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
239
240 if (exprNode_handleError (e))
241 {
242 return FALSE;
243 }
244
245 data = e->edata;
246
247 ret = TRUE;
248
249 switch (e->kind)
250 {
251
252 case XPR_FOR:
253 // ret = message ("%s %s",
254 exprNode_generateConstraints (exprData_getPairA (data));
255 exprNode_generateConstraints (exprData_getPairB (data));
256 break;
257
258 case XPR_FORPRED:
259 // ret = message ("for (%s; %s; %s)",
260 exprNode_generateConstraints (exprData_getTripleInit (data));
261 exprNode_generateConstraints (exprData_getTripleTest (data));
262 exprNode_generateConstraints (exprData_getTripleInc (data));
263 break;
264 case XPR_IF:
361091cc 265 DPRINTF(( "IF:") );
266 DPRINTF ((exprNode_unparse(e) ) );
4cccc6ad 267 // ret = message ("if (%s) %s",
268 exprNode_generateConstraints (exprData_getPairA (data));
269 exprNode_generateConstraints (exprData_getPairB (data));
270 // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
271 break;
272
273 case XPR_IFELSE:
274 // ret = message ("if (%s) %s else %s",
275 exprNode_generateConstraints (exprData_getTriplePred (data));
276 exprNode_generateConstraints (exprData_getTripleTrue (data));
277 exprNode_generateConstraints (exprData_getTripleFalse (data));
278 break;
279 case XPR_WHILE:
280 // ret = message ("while (%s) %s",
281 exprNode_generateConstraints (exprData_getPairA (data));
282 exprNode_generateConstraints (exprData_getPairB (data));
283 // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), exprData_getPairB (data) );
284 break;
285
286 case XPR_WHILEPRED:
287 // ret =
288 // cstring_copy (
289 exprNode_generateConstraints (exprData_getSingle (data));
290 break;
291
292 case XPR_DOWHILE:
293 // ret = message ("do { %s } while (%s)",
294 exprNode_generateConstraints (exprData_getPairB (data));
295 exprNode_generateConstraints (exprData_getPairA (data));
296 break;
297
298 case XPR_BLOCK:
299 // ret = message ("{ %s }",
300 exprNode_generateConstraints (exprData_getSingle (data));
361091cc 301 e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
302 e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
303 // e->constraints = (exprData_getSingle (data))->constraints;
4cccc6ad 304 break;
305
306 case XPR_STMT:
307 case XPR_STMTLIST:
308 return exprNode_stmtList (e);
309 /*@notreached@*/
310 break;
311 default:
312 ret=FALSE;
313 }
314 return ret;
315}
316
317
4cccc6ad 318bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint)
319{
320 exprNode t1, t2;
321
322 bool handledExprNode;
4cccc6ad 323 exprData data;
4cccc6ad 324 constraint cons;
325
326 DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
327 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
361091cc 328
329 e->requiresConstraints = constraintList_new();
330 e->ensuresConstraints = constraintList_new();
4cccc6ad 331
332 if (exprNode_handleError (e))
333 {
334 return FALSE;
335 }
336
337 handledExprNode = TRUE;
338
339 data = e->edata;
340
341 switch (e->kind)
342 {
343
344 case XPR_FETCH:
345
4cccc6ad 346 if (definatelv )
347 {
348 t1 = (exprData_getPairA (data) );
349 t2 = (exprData_getPairB (data) );
361091cc 350 cons = constraint_makeWriteSafeExprNode (t1, t2);
4cccc6ad 351 }
352 else
353 {
354 t1 = (exprData_getPairA (data) );
355 t2 = (exprData_getPairB (data) );
361091cc 356 cons = constraint_makeReadSafeExprNode (t1, t2 );
4cccc6ad 357 }
361091cc 358
359 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
4cccc6ad 360 cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
361091cc 361 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
bf92e32c 362 // cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
363 // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
361091cc 364
4cccc6ad 365 exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
366 exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
367
368 /*@i325 Should check which is array/index. */
4cccc6ad 369 break;
370 case XPR_PREOP:
371 t1 = exprData_getUopNode(data);
372 lltok_unparse (exprData_getUopTok (data));
373 exprNode_exprTraverse (exprData_getUopNode (data), definatelv, definaterv, sequencePoint );
374 /*handle * pointer access */
375
376 /*@ i 325 do ++ and -- */
377 if (lltok_isMult( exprData_getUopTok (data) ) )
378 {
379 if (definatelv)
380 {
361091cc 381 cons = constraint_makeWriteSafeInt (t1, 0);
4cccc6ad 382 }
383 else
384 {
385 cons = constraint_makeReadSafeInt (t1, 0);
4cccc6ad 386 }
361091cc 387 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
388 }
389 if (lltok_isInc_Op (exprData_getUopTok (data) ) )
390 {
391 // cons = constraint_makeSideEffectPostIncrement (t1, sequencePoint);
392 // e->ensuresConstraints = constraintList_add(e->requiresConstraints, cons);
4cccc6ad 393 }
4cccc6ad 394 break;
395
396 case XPR_PARENS:
397 exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
361091cc 398 // e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
bf92e32c 399 break;
4cccc6ad 400 case XPR_ASSIGN:
401 exprNode_exprTraverse (exprData_getOpA (data), TRUE, definaterv, sequencePoint );
402 lltok_unparse (exprData_getOpTok (data));
403 exprNode_exprTraverse (exprData_getOpB (data), definatelv, TRUE, sequencePoint );
361091cc 404 // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data) );
4cccc6ad 405 break;
406 case XPR_OP:
407 exprNode_exprTraverse (exprData_getOpA (data), definatelv, definaterv, sequencePoint );
408 lltok_unparse (exprData_getOpTok (data));
409 exprNode_exprTraverse (exprData_getOpB (data), definatelv, definaterv, sequencePoint );
410
361091cc 411 // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
4cccc6ad 412 break;
413 case XPR_SIZEOFT:
414 ctype_unparse (qtype_getType (exprData_getType (data) ) );
415
416 break;
417
418 case XPR_SIZEOF:
419 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
361091cc 420 // e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
4cccc6ad 421 break;
422
423 case XPR_CALL:
424 exprNode_exprTraverse (exprData_getFcn (data), definatelv, definaterv, sequencePoint );
425 exprNodeList_unparse (exprData_getArgs (data) );
426 // e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) );
427 break;
428
429 case XPR_RETURN:
430 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
431 break;
432
433 case XPR_NULLRETURN:
434 cstring_makeLiteral ("return");;
435 break;
436
437
438 case XPR_FACCESS:
439 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
440 exprData_getFieldName (data) ;
441 break;
442
443 case XPR_ARROW:
444 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
445 exprData_getFieldName (data);
446 break;
447
448 case XPR_STRINGLITERAL:
449 cstring_copy (exprData_getLiteral (data));
450 break;
451
452 case XPR_NUMLIT:
453 cstring_copy (exprData_getLiteral (data));
454 break;
455 case XPR_POSTOP:
456
457 exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
458 lltok_unparse (exprData_getUopTok (data));
4cccc6ad 459 if (lltok_isInc_Op (exprData_getUopTok (data) ) )
460 {
bf92e32c 461 DPRINTF(("doing ++"));
4cccc6ad 462 t1 = exprData_getUopNode (data);
361091cc 463 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
464 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
bf92e32c 465 // cons = constraint_makeMaxReadSideEffectPostIncrement (t1, sequencePoint );
466 //e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
4cccc6ad 467 }
468 break;
469 default:
470 handledExprNode = FALSE;
471 }
472
bf92e32c 473 e->requiresConstraints = constraintList_preserveOrig ( e->requiresConstraints);
474 e->ensuresConstraints = constraintList_preserveOrig ( e->ensuresConstraints);
475
4cccc6ad 476 return handledExprNode;
477}
478
361091cc 479/* walk down the tree and get all requires Constraints in each subexpression*/
480constraintList exprNode_traversRequiresConstraints (exprNode e)
481{
482 // exprNode t1, t2;
483
484 bool handledExprNode;
485 // char * mes;
486 exprData data;
487 constraintList ret;
488 ret = constraintList_copy (e->requiresConstraints );
489 if (exprNode_handleError (e))
490 {
491 return ret;
492 }
493
494 handledExprNode = TRUE;
495
496 data = e->edata;
497
498 switch (e->kind)
499 {
500
501 case XPR_FETCH:
502
503 ret = constraintList_addList (ret,
504 exprNode_traversRequiresConstraints
505 (exprData_getPairA (data) ) );
506
507 ret = constraintList_addList (ret,
508 exprNode_traversRequiresConstraints
509 (exprData_getPairB (data) ) );
510 break;
511 case XPR_PREOP:
512
513 ret = constraintList_addList (ret,
514 exprNode_traversRequiresConstraints
515 (exprData_getUopNode (data) ) );
516 break;
517
518 case XPR_PARENS:
519 ret = constraintList_addList (ret, exprNode_traversRequiresConstraints
520 (exprData_getUopNode (data) ) );
521 break;
522 case XPR_ASSIGN:
523 ret = constraintList_addList (ret,
524 exprNode_traversRequiresConstraints
525 (exprData_getOpA (data) ) );
526
527 ret = constraintList_addList (ret,
528 exprNode_traversRequiresConstraints
529 (exprData_getOpB (data) ) );
530 break;
531 case XPR_OP:
532 ret = constraintList_addList (ret,
533 exprNode_traversRequiresConstraints
534 (exprData_getOpA (data) ) );
535
536 ret = constraintList_addList (ret,
537 exprNode_traversRequiresConstraints
538 (exprData_getOpB (data) ) );
539 break;
540 case XPR_SIZEOFT:
541
542 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
543
544 break;
545
546 case XPR_SIZEOF:
547
548 ret = constraintList_addList (ret,
549 exprNode_traversRequiresConstraints
550 (exprData_getSingle (data) ) );
551 break;
552
553 case XPR_CALL:
554 ret = constraintList_addList (ret,
555 exprNode_traversRequiresConstraints
556 (exprData_getFcn (data) ) );
557 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
558 break;
559
560 case XPR_RETURN:
561 ret = constraintList_addList (ret,
562 exprNode_traversRequiresConstraints
563 (exprData_getSingle (data) ) );
564 break;
565
566 case XPR_NULLRETURN:
567 // cstring_makeLiteral ("return");;
568 break;
569
570 case XPR_FACCESS:
571 ret = constraintList_addList (ret,
572 exprNode_traversRequiresConstraints
573 (exprData_getFieldNode (data) ) );
574 //exprData_getFieldName (data) ;
575 break;
576
577 case XPR_ARROW:
578 ret = constraintList_addList (ret,
579 exprNode_traversRequiresConstraints
580 (exprData_getFieldNode (data) ) );
581 // exprData_getFieldName (data);
582 break;
583
584 case XPR_STRINGLITERAL:
585 // cstring_copy (exprData_getLiteral (data));
586 break;
587
588 case XPR_NUMLIT:
589 // cstring_copy (exprData_getLiteral (data));
590 break;
591 case XPR_POSTOP:
592
593 ret = constraintList_addList (ret,
594 exprNode_traversRequiresConstraints
595 (exprData_getUopNode (data) ) );
596 break;
597 default:
598 break;
599 }
600
601 return ret;
602}
603
604
605/* walk down the tree and get all Ensures Constraints in each subexpression*/
606constraintList exprNode_traversEnsuresConstraints (exprNode e)
607{
608 // exprNode t1, t2;
609
610 bool handledExprNode;
611 // char * mes;
612 exprData data;
613 // constraintExpr tmp;
614 // constraint cons;
615 constraintList ret;
616 ret = constraintList_copy (e->ensuresConstraints );
617 if (exprNode_handleError (e))
618 {
619 return ret;
620 }
621
622 handledExprNode = TRUE;
623
624 data = e->edata;
625
626 DPRINTF( (message (
627 "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
628 exprNode_unparse (e),
629 constraintList_print(e->ensuresConstraints)
630 )
631 ));
632
633
634 switch (e->kind)
635 {
636
637 case XPR_FETCH:
638
639 ret = constraintList_addList (ret,
640 exprNode_traversEnsuresConstraints
641 (exprData_getPairA (data) ) );
642
643 ret = constraintList_addList (ret,
644 exprNode_traversEnsuresConstraints
645 (exprData_getPairB (data) ) );
646 break;
647 case XPR_PREOP:
648
649 ret = constraintList_addList (ret,
650 exprNode_traversEnsuresConstraints
651 (exprData_getUopNode (data) ) );
652 break;
653
654 case XPR_PARENS:
655 ret = constraintList_addList (ret, exprNode_traversEnsuresConstraints
656 (exprData_getUopNode (data) ) );
657 break;
658 case XPR_ASSIGN:
659 ret = constraintList_addList (ret,
660 exprNode_traversEnsuresConstraints
661 (exprData_getOpA (data) ) );
662
663 ret = constraintList_addList (ret,
664 exprNode_traversEnsuresConstraints
665 (exprData_getOpB (data) ) );
666 break;
667 case XPR_OP:
668 ret = constraintList_addList (ret,
669 exprNode_traversEnsuresConstraints
670 (exprData_getOpA (data) ) );
671
672 ret = constraintList_addList (ret,
673 exprNode_traversEnsuresConstraints
674 (exprData_getOpB (data) ) );
675 break;
676 case XPR_SIZEOFT:
677
678 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
679
680 break;
681
682 case XPR_SIZEOF:
683
684 ret = constraintList_addList (ret,
685 exprNode_traversEnsuresConstraints
686 (exprData_getSingle (data) ) );
687 break;
688
689 case XPR_CALL:
690 ret = constraintList_addList (ret,
691 exprNode_traversEnsuresConstraints
692 (exprData_getFcn (data) ) );
693 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
694 break;
695
696 case XPR_RETURN:
697 ret = constraintList_addList (ret,
698 exprNode_traversEnsuresConstraints
699 (exprData_getSingle (data) ) );
700 break;
701
702 case XPR_NULLRETURN:
703 // cstring_makeLiteral ("return");;
704 break;
705
706 case XPR_FACCESS:
707 ret = constraintList_addList (ret,
708 exprNode_traversEnsuresConstraints
709 (exprData_getFieldNode (data) ) );
710 //exprData_getFieldName (data) ;
711 break;
712
713 case XPR_ARROW:
714 ret = constraintList_addList (ret,
715 exprNode_traversEnsuresConstraints
716 (exprData_getFieldNode (data) ) );
717 // exprData_getFieldName (data);
718 break;
719
720 case XPR_STRINGLITERAL:
721 // cstring_copy (exprData_getLiteral (data));
722 break;
723
724 case XPR_NUMLIT:
725 // cstring_copy (exprData_getLiteral (data));
726 break;
727 case XPR_POSTOP:
728
729 ret = constraintList_addList (ret,
730 exprNode_traversEnsuresConstraints
731 (exprData_getUopNode (data) ) );
732 break;
733 default:
734 break;
735 }
736DPRINTF( (message (
737 "exprnode_traversEnsuresConstraints call for %s with constraintList of is returning %s",
738 exprNode_unparse (e),
739 // constraintList_print(e->ensuresConstraints),
740 constraintList_print(ret)
741 )
742 ));
743
744
745 return ret;
746}
747
git-cvsimport mirror of splint
This page took 0.185386 seconds and 5 git commands to generate.