]> andersk Git - splint.git/blame_incremental - src/constraintTerm.c
noexpand always false.
[splint.git] / src / constraintTerm.c
... / ...
CommitLineData
1/*
2** Splint - annotation-assisted static program checker
3** Copyright (C) 1994-2003 University of Virginia,
4** Massachusetts Institute of Technology
5**
6** This program is free software; you can redistribute it and/or modify it
7** under the terms of the GNU General Public License as published by the
8** Free Software Foundation; either version 2 of the License, or (at your
9** option) any later version.
10**
11** This program is distributed in the hope that it will be useful, but
12** WITHOUT ANY WARRANTY; without even the implied warranty of
13** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14** General Public License for more details.
15**
16** The GNU General Public License is available from http://www.gnu.org/ or
17** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
18** MA 02111-1307, USA.
19**
20** For information on splint: info@splint.org
21** To report a bug: splint-bug@splint.org
22** For more information: http://www.splint.org
23*/
24
25/*
26** constraintTerm.c
27*/
28
29/* #define DEBUGPRINT 1 */
30
31# include <ctype.h> /* for isdigit */
32# include "splintMacros.nf"
33# include "basic.h"
34# include "cgrammar.h"
35# include "cgrammar_tokens.h"
36
37# include "exprChecks.h"
38# include "exprNodeSList.h"
39
40bool constraintTerm_isDefined (constraintTerm t)
41{
42 return t != NULL;
43}
44
45void constraintTerm_free (/*@only@*/ constraintTerm term)
46{
47 llassert (constraintTerm_isDefined (term));
48
49 fileloc_free (term->loc);
50
51 switch (term->kind)
52 {
53 case CTT_EXPR:
54 /* we don't free an exprNode*/
55 break;
56 case CTT_SREF:
57 /* sref */
58 sRef_free (term->value.sref);
59 break;
60 case CTT_INTLITERAL:
61 /* don't free an int */
62 break;
63 case CTT_ERRORBADCONSTRAINTTERMTYPE:
64 default:
65 /* type was set incorrectly */
66 llcontbug (message("constraintTerm_free type was set incorrectly"));
67 }
68
69 term->kind = CTT_ERRORBADCONSTRAINTTERMTYPE;
70 free (term);
71}
72
73/*@only@*/ static/*@out@*/ constraintTerm new_constraintTermExpr (void)
74{
75 constraintTerm ret;
76 ret = dmalloc (sizeof (* ret ) );
77 ret->value.intlit = 0;
78 return ret;
79}
80
81
82bool constraintTerm_isIntLiteral (constraintTerm term)
83{
84 llassert(term != NULL);
85
86 if (term->kind == CTT_INTLITERAL)
87 return TRUE;
88
89 return FALSE;
90}
91
92
93bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
94{
95 llassert (c != NULL);
96
97 if (c->kind == CTT_EXPR)
98 {
99 if (exprNode_isInitBlock (c->value.expr))
100 {
101 return TRUE;
102 }
103 }
104 return FALSE;
105}
106
107
108bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
109{
110 llassert (c != NULL);
111
112 if (c->kind == CTT_EXPR)
113 {
114 return TRUE;
115 }
116 return FALSE;
117}
118
119/*@access exprNode@*/
120int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
121{
122 exprNodeList list;
123 int ret;
124 llassert (c != NULL);
125 llassert (constraintTerm_isInitBlock (c) );
126 llassert (c->kind == CTT_EXPR);
127
128 llassert(exprNode_isDefined(c->value.expr) );
129
130 if (exprNode_isUndefined(c->value.expr) )
131 {
132 return 1;
133 }
134
135 if (c->value.expr->edata == exprData_undefined)
136 {
137 return 1;
138 }
139 list = exprData_getArgs(c->value.expr->edata);
140
141 ret = exprNodeList_size(list);
142
143 return ret;
144}
145/*@noaccess exprNode@*/
146
147
148bool constraintTerm_isStringLiteral (constraintTerm c) /*@*/
149{
150 llassert (c != NULL);
151 if (c->kind == CTT_EXPR)
152 {
153 if (exprNode_knownStringValue(c->value.expr) )
154 {
155 return TRUE;
156 }
157 }
158 return FALSE;
159}
160
161
162
163cstring constraintTerm_getStringLiteral (constraintTerm c)
164{
165 llassert (c != NULL);
166 llassert (constraintTerm_isStringLiteral (c) );
167 llassert (c->kind == CTT_EXPR);
168
169 return (cstring_copy ( multiVal_forceString (exprNode_getValue (c->value.expr) ) ) );
170}
171
172constraintTerm constraintTerm_simplify (/*@returned@*/ constraintTerm term) /*@modifies term@*/
173{
174 if (term->kind == CTT_EXPR)
175 {
176 if ( exprNode_knownIntValue (term->value.expr ) )
177 {
178 long int temp;
179
180 temp = exprNode_getLongValue (term->value.expr);
181 term->value.intlit = (int)temp;
182 term->kind = CTT_INTLITERAL;
183 }
184 }
185 return term;
186}
187
188fileloc constraintTerm_getFileloc (constraintTerm t)
189{
190 llassert (constraintTerm_isDefined (t));
191 return (fileloc_copy (t->loc) );
192}
193
194constraintTermType constraintTerm_getKind (constraintTerm t)
195{
196 llassert (constraintTerm_isDefined(t) );
197
198 return (t->kind);
199}
200
201/*@exposed@*/ sRef constraintTerm_getSRef (constraintTerm t)
202{
203 llassert (constraintTerm_isDefined(t) );
204 llassert (t->kind == CTT_SREF);
205
206 return (t->value.sref);
207}
208
209/*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@dependent@*/ exprNode e)
210{
211 constraintTerm ret = new_constraintTermExpr ();
212 ret->loc = fileloc_copy (exprNode_loc (e));
213 ret->value.expr = e;
214 ret->kind = CTT_EXPR;
215 ret = constraintTerm_simplify (ret);
216 return ret;
217}
218
219/*@only@*/ constraintTerm constraintTerm_makesRef (/*@temp@*/ /*@observer@*/ sRef s)
220{
221 constraintTerm ret = new_constraintTermExpr();
222 ret->loc = fileloc_undefined;
223 ret->value.sref = sRef_saveCopy(s);
224 ret->kind = CTT_SREF;
225 ret = constraintTerm_simplify(ret);
226 return ret;
227}
228
229
230
231constraintTerm constraintTerm_copy (constraintTerm term)
232{
233 constraintTerm ret;
234 ret = new_constraintTermExpr();
235 ret->loc = fileloc_copy (term->loc);
236
237 switch (term->kind)
238 {
239 case CTT_EXPR:
240 ret->value.expr = term->value.expr;
241 break;
242 case CTT_INTLITERAL:
243 ret->value.intlit = term->value.intlit;
244 break;
245
246 case CTT_SREF:
247 ret->value.sref = sRef_saveCopy(term->value.sref);
248 break;
249 default:
250 BADEXIT;
251 }
252 ret->kind = term->kind;
253 return ret;
254}
255
256constraintTerm constraintTerm_setFileloc (/*@returned@*/ constraintTerm term, fileloc loc)
257{
258 llassert(term != NULL);
259
260 if ( fileloc_isDefined( term->loc ) )
261 fileloc_free(term->loc);
262
263 term->loc = fileloc_copy(loc);
264 return term;
265}
266
267
268static cstring constraintTerm_getName (constraintTerm term)
269{
270 cstring s;
271 s = cstring_undefined;
272
273 llassert (term != NULL);
274
275 switch (term->kind)
276 {
277 case CTT_EXPR:
278
279 s = message ("%s", exprNode_unparse (term->value.expr) );
280 break;
281 case CTT_INTLITERAL:
282 s = message (" %d ", (int) term->value.intlit);
283 break;
284
285 case CTT_SREF:
286 s = message ("%q", sRef_unparse (term->value.sref) );
287
288 break;
289 default:
290 BADEXIT;
291 /*@notreached@*/
292 break;
293 }
294
295 return s;
296}
297
298constraintTerm
299constraintTerm_doSRefFixBaseParam (/*@returned@*/constraintTerm term, exprNodeList arglist) /*@modifies term@*/
300{
301 llassert (term != NULL);
302
303 switch (term->kind)
304 {
305 case CTT_EXPR:
306
307 break;
308 case CTT_INTLITERAL:
309 break;
310
311 case CTT_SREF:
312 term->value.sref = sRef_fixBaseParam (term->value.sref, arglist);
313 break;
314 default:
315 BADEXIT;
316 }
317 return term;
318
319}
320
321cstring constraintTerm_unparse (constraintTerm term) /*@*/
322{
323 cstring s;
324 s = cstring_undefined;
325
326 llassert (term != NULL);
327
328 switch (term->kind)
329 {
330 case CTT_EXPR:
331
332 s = message ("%s @ %q", exprNode_unparse (term->value.expr),
333 fileloc_unparse (term->loc) );
334 break;
335 case CTT_INTLITERAL:
336 s = message ("%d", (int)term->value.intlit);
337 break;
338
339 case CTT_SREF:
340 s = message ("%q", sRef_unparseDebug (term->value.sref) );
341
342 break;
343 default:
344 BADEXIT;
345 }
346
347 return s;
348}
349
350
351constraintTerm constraintTerm_makeIntLiteral (long i)
352{
353 constraintTerm ret = new_constraintTermExpr();
354 ret->value.intlit = i;
355 ret->kind = CTT_INTLITERAL;
356 ret->loc = fileloc_undefined;
357 return ret;
358}
359
360bool constraintTerm_canGetValue (constraintTerm term)
361{
362 if (term->kind == CTT_INTLITERAL)
363 {
364 return TRUE;
365 }
366 else if (term->kind == CTT_SREF)
367 {
368 if (sRef_hasValue (term->value.sref))
369 {
370 multiVal mval = sRef_getValue (term->value.sref);
371
372 return multiVal_isInt (mval); /* for now, only try to deal with int values */
373 }
374 else
375 {
376 return FALSE;
377 }
378 }
379 else if (term->kind == CTT_EXPR)
380 {
381 return FALSE;
382 }
383 else
384 {
385 return FALSE;
386 }
387}
388
389void constraintTerm_setValue (constraintTerm term, long value)
390{
391 if (term->kind == CTT_INTLITERAL)
392 {
393 term->value.intlit = value;
394 }
395 else
396 {
397 BADBRANCH;
398 }
399}
400
401long constraintTerm_getValue (constraintTerm term)
402{
403 llassert (constraintTerm_canGetValue (term));
404
405 if (term->kind == CTT_INTLITERAL)
406 {
407 return term->value.intlit;
408 }
409 else if (term->kind == CTT_SREF)
410 {
411 if (sRef_hasValue (term->value.sref))
412 {
413 multiVal mval = sRef_getValue (term->value.sref);
414
415 return multiVal_forceInt (mval); /* for now, only try to deal with int values */
416 }
417 else
418 {
419 BADBRANCH;
420 }
421 }
422 else if (term->kind == CTT_EXPR)
423 {
424 BADBRANCH;
425 }
426 else
427 {
428 BADBRANCH;
429 }
430
431 BADEXIT;
432}
433
434/*drl added this 10.30.001
435 */
436
437/*@exposed@*/ exprNode constraintTerm_getExprNode (constraintTerm t)
438{
439 llassert (t != NULL);
440
441 llassert (t->kind == CTT_EXPR);
442
443 return t->value.expr;
444
445}
446
447 /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t)
448{
449 llassert (t != NULL);
450 if (t->kind == CTT_EXPR)
451 {
452 return exprNode_getSref(t->value.expr);
453 }
454
455 if (t->kind == CTT_SREF)
456 {
457 return t->value.sref;
458 }
459
460 return sRef_undefined;
461}
462
463bool constraintTerm_probSame (constraintTerm term1, constraintTerm term2)
464{
465 cstring s1, s2;
466
467 llassert (term1 !=NULL && term2 !=NULL);
468
469 DPRINTF ((message
470 ("Comparing srefs for %s and %s ", constraintTerm_getName(term1), constraintTerm_getName(term2)
471 )
472 )
473 );
474
475 s1 = constraintTerm_getName (term1);
476 s2 = constraintTerm_getName (term2);
477
478 if (cstring_equal (s1, s2) )
479 {
480 DPRINTF ((message (" %q and %q are same", s1, s2 ) ) );
481 return TRUE;
482 }
483 else
484 {
485 DPRINTF ((message (" %q and %q are not same", s1, s2 ) ) );
486 return FALSE;
487 }
488}
489
490bool constraintTerm_similar (constraintTerm term1, constraintTerm term2)
491{
492 sRef s1, s2;
493
494 llassert (term1 !=NULL && term2 !=NULL);
495
496 if (constraintTerm_canGetValue (term1) && constraintTerm_canGetValue (term2))
497
498 /*3/30/2003 comment updated to reflect name change form INTLITERAL to CTT_INTLITERAL*/
499 /* evans 2001-07-24: was (term1->kind == CTT_INTLITERAL) && (term2->kind == CTT_INTLITERAL) ) */
500 {
501 long t1, t2;
502
503 t1 = constraintTerm_getValue (term1);
504 t2 = constraintTerm_getValue (term2);
505
506 return (t1 == t2);
507 }
508
509 /*drl this if statement handles the case where constraintTerm_canGetValue only returns
510 true for term1 or term2 but no both
511 if constraintTerm_canGetValue returned tru for both we would have returned in the previous if statement
512 I suppose this could be done with xor but I've never used xor and don't feel like starting now
513 besides this way is more effecient.
514 */
515 if (constraintTerm_canGetValue (term1) || constraintTerm_canGetValue (term2))
516 {
517
518 return FALSE;
519 }
520
521 s1 = constraintTerm_getsRef (term1);
522 s2 = constraintTerm_getsRef (term2);
523
524 if (!(sRef_isValid(s1) && sRef_isValid(s2)))
525 {
526 return FALSE;
527 }
528
529 DPRINTF((message
530 ("Comparing srefs for %s and %s ", constraintTerm_getName(term1), constraintTerm_getName(term2)
531 )
532 )
533 );
534
535 if (sRef_similarRelaxed(s1, s2) || sRef_sameName (s1, s2) )
536 {
537 DPRINTF ((message (" %s and %s are same", constraintTerm_getName(term1), constraintTerm_getName(term2) ) ));
538 return TRUE;
539 }
540 else
541 {
542 DPRINTF ((message (" %s and %s are not same", constraintTerm_getName(term1), constraintTerm_getName(term2) ) ));
543 return FALSE;
544 }
545}
546
547void constraintTerm_dump (/*@observer@*/ constraintTerm t, FILE *f)
548{
549 fileloc loc;
550 constraintTermValue value;
551 constraintTermType kind;
552 uentry u;
553
554 loc = t->loc;
555
556 value = t->value;
557
558 kind = t->kind;
559
560 fprintf(f, "%d\n", (int) kind);
561
562 switch (kind)
563 {
564
565 case CTT_EXPR:
566 u = exprNode_getUentry(t->value.expr);
567 fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u)));
568 break;
569
570 case CTT_SREF:
571 {
572 sRef s;
573
574 s = t->value.sref;
575
576 if (sRef_isResult (s ) )
577 {
578 fprintf(f, "Result\n");
579 }
580 else if (sRef_isParam (s))
581 {
582 int param;
583 ctype ct;
584 cstring ctString;
585
586
587 ct = sRef_getType (s);
588 param = sRef_getParam(s);
589
590 ctString = ctype_dump(ct);
591
592 fprintf(f, "Param %s %d\n", cstring_toCharsSafe(ctString), (int) param );
593 cstring_free(ctString);
594 }
595 else if (sRef_isField (s) )
596 {
597 fprintf(f, "sRef_dump %s\n", cstring_toCharsSafe(sRef_dump(s)) );
598 }
599 else
600 {
601 u = sRef_getUentry(s);
602 fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u)));
603 }
604
605 }
606 break;
607
608 case CTT_INTLITERAL:
609 fprintf (f, "%ld\n", t->value.intlit);
610 break;
611
612 default:
613 BADEXIT;
614 }
615
616}
617
618
619/*@only@*/ constraintTerm constraintTerm_undump (FILE *f)
620{
621 constraintTermType kind;
622 constraintTerm ret;
623
624 uentry ue;
625
626 char *str;
627 char *os;
628
629 os = mstring_create (MAX_DUMP_LINE_LENGTH);
630
631 str = fgets (os, MAX_DUMP_LINE_LENGTH, f);
632
633 llassert (str != NULL);
634
635 kind = (constraintTermType) reader_getInt(&str);
636 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
637
638 llassert (str != NULL);
639
640 switch (kind)
641 {
642
643 case CTT_SREF:
644 {
645 sRef s;
646 char * term;
647 term = reader_getWord(&str);
648
649 if (term == NULL)
650 {
651 llfatalbug (message ("Library file appears to be corrupted.") );
652 }
653 if (strcmp (term, "Result") == 0 )
654 {
655 s = sRef_makeResult (ctype_unknown);
656 }
657 else if (strcmp (term, "Param" ) == 0 )
658 {
659 int param;
660 char *str2, *ostr2;
661
662 ctype t;
663
664 reader_checkChar(&str, ' ');
665 str2 = reader_getWord(&str);
666 param = reader_getInt(&str);
667
668 if (str2 == NULL)
669 {
670 llfatalbug (message ("Library file appears to be corrupted.") );
671 }
672
673 ostr2 = str2;
674 t = ctype_undump(&str2) ;
675 s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc, SA_CREATED));
676 free (ostr2);
677 }
678 else if (strcmp (term, "sRef_dump" ) == 0 )
679 {
680 reader_checkChar(&str, ' ');
681 s = sRef_undump (&str);
682 }
683 else /* This must be an identified that we can search for in usymTab */
684 {
685 cstring termStr = cstring_makeLiteralTemp(term);
686
687 ue = usymtab_lookup (termStr);
688 s = uentry_getSref(ue);
689 }
690
691 ret = constraintTerm_makesRef(s);
692
693 free(term);
694 }
695 break;
696
697 case CTT_EXPR:
698 {
699 sRef s;
700 char * term;
701 cstring termStr;
702
703 term = reader_getWord(&str);
704
705 if (term == NULL)
706 {
707 llfatalbug (message ("Library file appears to be corrupted.") );
708 }
709
710 /* This must be an identifier that we can search for in usymTab */
711 termStr = cstring_makeLiteralTemp(term);
712
713 ue = usymtab_lookup (termStr);
714 s = uentry_getSref(ue);
715 ret = constraintTerm_makesRef(s);
716
717 free (term);
718 }
719 break;
720
721
722 case CTT_INTLITERAL:
723 {
724 int i;
725
726 i = reader_getInt(&str);
727 ret = constraintTerm_makeIntLiteral (i);
728 }
729 break;
730
731 default:
732 BADEXIT;
733 }
734 free (os);
735
736 return ret;
737}
738
739
740
741/* drl added sometime before 10/17/001*/
742ctype constraintTerm_getCType (constraintTerm term)
743{
744 ctype ct;
745
746 switch (term->kind)
747 {
748 case CTT_EXPR:
749 ct = exprNode_getType (term->value.expr);
750 break;
751
752 case CTT_INTLITERAL:
753 ct = ctype_signedintegral;
754 break;
755
756 case CTT_SREF:
757 ct = sRef_getType (term->value.sref) ;
758 break;
759 default:
760 BADEXIT;
761 }
762 return ct;
763}
764
765bool constraintTerm_isConstantOnly (constraintTerm term)
766{
767 switch (term->kind)
768 {
769 case CTT_EXPR:
770 if (exprNode_isNumLiteral (term->value.expr) ||
771 exprNode_isStringLiteral (term->value.expr) ||
772 exprNode_isCharLiteral (term->value.expr) )
773 {
774 return TRUE;
775 }
776 else
777 {
778 return FALSE;
779 }
780
781 case CTT_INTLITERAL:
782 return TRUE;
783
784 case CTT_SREF:
785 if ( sRef_isConst (term->value.sref) )
786 {
787 return TRUE;
788 }
789 else
790 {
791 return FALSE;
792 }
793 default:
794 BADEXIT;
795 }
796
797 BADEXIT;
798}
This page took 0.113475 seconds and 5 git commands to generate.