2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2002 University of Virginia,
4 ** Massachusetts Institute of Technology
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.
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.
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.
20 ** For information on splint: splint@cs.virginia.edu
21 ** To report a bug: splint-bug@cs.virginia.edu
22 ** For more information: http://www.splint.org
29 /* #define DEBUGPRINT 1 */
31 # include <ctype.h> /* for isdigit */
32 # include "splintMacros.nf"
34 # include "cgrammar.h"
35 # include "cgrammar_tokens.h"
37 # include "exprChecks.h"
38 # include "exprNodeSList.h"
42 /*@access exprNode @*/
44 bool constraintTerm_isDefined (constraintTerm t)
49 void constraintTerm_free (/*@only@*/ constraintTerm term)
51 llassert (constraintTerm_isDefined (term));
53 fileloc_free (term->loc);
58 /* we don't free an exprNode*/
62 sRef_free (term->value.sref);
65 /* don't free an int */
67 case ERRORBADCONSTRAINTTERMTYPE:
69 /* type was set incorrectly */
70 llcontbug (message("constraintTerm_free type was set incorrectly"));
73 term->kind = ERRORBADCONSTRAINTTERMTYPE;
77 /*@only@*/ static/*@out@*/ constraintTerm new_constraintTermExpr (void)
80 ret = dmalloc (sizeof (* ret ) );
81 ret->value.intlit = 0;
86 bool constraintTerm_isIntLiteral (constraintTerm term)
88 llassert(term != NULL);
90 if (term->kind == INTLITERAL)
97 bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
100 if (c->kind == EXPRNODE)
103 if (exprNode_isInitBlock(c->value.expr) )
112 bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
114 llassert (c != NULL);
115 if (c->kind == EXPRNODE)
123 int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
128 llassert (c != NULL);
129 llassert (constraintTerm_isInitBlock (c) );
130 llassert (c->kind == EXPRNODE);
132 llassert(exprNode_isDefined(c->value.expr) );
134 if (exprNode_isUndefined(c->value.expr) )
139 if (c->value.expr->edata == exprData_undefined)
143 list = exprData_getArgs(c->value.expr->edata);
145 ret = exprNodeList_size(list);
152 bool constraintTerm_isStringLiteral (constraintTerm c) /*@*/
154 llassert (c != NULL);
155 if (c->kind == EXPRNODE)
157 if (exprNode_knownStringValue(c->value.expr) )
167 cstring constraintTerm_getStringLiteral (constraintTerm c)
169 llassert (c != NULL);
170 llassert (constraintTerm_isStringLiteral (c) );
171 llassert (c->kind == EXPRNODE);
173 return (cstring_copy ( multiVal_forceString (exprNode_getValue (c->value.expr) ) ) );
176 constraintTerm constraintTerm_simplify (/*@returned@*/ constraintTerm term) /*@modifies term@*/
178 if (term->kind == EXPRNODE)
180 if ( exprNode_knownIntValue (term->value.expr ) )
184 temp = exprNode_getLongValue (term->value.expr);
185 term->value.intlit = (int)temp;
186 term->kind = INTLITERAL;
192 fileloc constraintTerm_getFileloc (constraintTerm t)
194 llassert (constraintTerm_isDefined (t));
195 return (fileloc_copy (t->loc) );
198 constraintTermType constraintTerm_getKind (constraintTerm t)
200 llassert (constraintTerm_isDefined(t) );
205 /*@exposed@*/ sRef constraintTerm_getSRef (constraintTerm t)
207 llassert (constraintTerm_isDefined(t) );
208 llassert (t->kind == SREF);
210 return (t->value.sref);
213 /*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@dependent@*/ exprNode e)
215 constraintTerm ret = new_constraintTermExpr();
216 ret->loc = fileloc_copy(exprNode_getfileloc(e));
218 ret->kind = EXPRNODE;
219 ret = constraintTerm_simplify(ret);
223 /*@only@*/ constraintTerm constraintTerm_makesRef (/*@temp@*/ /*@observer@*/ sRef s)
225 constraintTerm ret = new_constraintTermExpr();
226 ret->loc = fileloc_undefined;
227 ret->value.sref = sRef_saveCopy(s);
229 ret = constraintTerm_simplify(ret);
235 constraintTerm constraintTerm_copy (constraintTerm term)
238 ret = new_constraintTermExpr();
239 ret->loc = fileloc_copy (term->loc);
244 ret->value.expr = term->value.expr;
247 ret->value.intlit = term->value.intlit;
251 ret->value.sref = sRef_saveCopy(term->value.sref);
256 ret->kind = term->kind;
260 constraintTerm constraintTerm_setFileloc (/*@returned@*/ constraintTerm term, fileloc loc)
262 llassert(term != NULL);
264 if ( fileloc_isDefined( term->loc ) )
265 fileloc_free(term->loc);
267 term->loc = fileloc_copy(loc);
272 static cstring constraintTerm_getName (constraintTerm term)
275 s = cstring_undefined;
277 llassert (term != NULL);
283 s = message ("%s", exprNode_unparse (term->value.expr) );
286 s = message (" %d ", (int) term->value.intlit);
290 s = message ("%q", sRef_unparse (term->value.sref) );
303 constraintTerm_doSRefFixBaseParam (/*@returned@*/constraintTerm term, exprNodeList arglist) /*@modifies term@*/
305 llassert (term != NULL);
316 term->value.sref = sRef_fixBaseParam (term->value.sref, arglist);
325 cstring constraintTerm_print (constraintTerm term) /*@*/
328 s = cstring_undefined;
330 llassert (term != NULL);
336 s = message ("%s @ %q", exprNode_unparse (term->value.expr),
337 fileloc_unparse (term->loc) );
340 s = message ("%d", (int)term->value.intlit);
344 s = message ("%q", sRef_unparseDebug (term->value.sref) );
355 constraintTerm constraintTerm_makeIntLiteral (long i)
357 constraintTerm ret = new_constraintTermExpr();
358 ret->value.intlit = i;
359 ret->kind = INTLITERAL;
360 ret->loc = fileloc_undefined;
364 bool constraintTerm_canGetValue (constraintTerm term)
366 if (term->kind == INTLITERAL)
370 else if (term->kind == SREF)
372 if (sRef_hasValue (term->value.sref))
374 multiVal mval = sRef_getValue (term->value.sref);
376 return multiVal_isInt (mval); /* for now, only try to deal with int values */
383 else if (term->kind == EXPRNODE)
393 long constraintTerm_getValue (constraintTerm term)
395 llassert (constraintTerm_canGetValue (term));
397 if (term->kind == INTLITERAL)
399 return term->value.intlit;
401 else if (term->kind == SREF)
403 if (sRef_hasValue (term->value.sref))
405 multiVal mval = sRef_getValue (term->value.sref);
407 return multiVal_forceInt (mval); /* for now, only try to deal with int values */
414 else if (term->kind == EXPRNODE)
426 /*drl added this 10.30.001
429 /*@exposed@*/ exprNode constraintTerm_getExprNode (constraintTerm t)
431 llassert (t != NULL);
433 llassert (t->kind == EXPRNODE);
435 return t->value.expr;
439 /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t)
441 llassert (t != NULL);
442 if (t->kind == EXPRNODE)
444 return exprNode_getSref(t->value.expr);
449 return t->value.sref;
452 return sRef_undefined;
455 bool constraintTerm_probSame (constraintTerm term1, constraintTerm term2)
459 llassert (term1 !=NULL && term2 !=NULL);
462 ("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2)
467 s1 = constraintTerm_getName (term1);
468 s2 = constraintTerm_getName (term2);
470 if (cstring_equal (s1, s2) )
472 DPRINTF ((message (" %q and %q are same", s1, s2 ) ) );
477 DPRINTF ((message (" %q and %q are not same", s1, s2 ) ) );
482 bool constraintTerm_similar (constraintTerm term1, constraintTerm term2)
486 llassert (term1 !=NULL && term2 !=NULL);
488 if (constraintTerm_canGetValue (term1) && constraintTerm_canGetValue (term2))
489 /* evans 2001-07-24: was (term1->kind == INTLITERAL) && (term2->kind == INTLITERAL) ) */
493 t1 = constraintTerm_getValue (term1);
494 t2 = constraintTerm_getValue (term2);
499 if (constraintTerm_canGetValue (term1) || constraintTerm_canGetValue (term2))
501 /* evans 2001-07-24: is this right? */ /*@i534@*/
505 s1 = constraintTerm_getsRef (term1);
506 s2 = constraintTerm_getsRef (term2);
508 if (!(sRef_isValid(s1) && sRef_isValid(s2)))
514 ("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2)
519 if (sRef_similarRelaxed(s1, s2) || sRef_sameName (s1, s2) )
521 DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2) ) ));
526 DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) ));
531 void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f)
534 constraintTermValue value;
535 constraintTermType kind;
544 fprintf(f, "%d\n", (int) kind);
550 u = exprNode_getUentry(t->value.expr);
551 fprintf(f, "%s\n", cstring_toCharsSafe( uentry_rawName (u) )
561 if (sRef_isResult (s ) )
563 fprintf(f, "Result\n");
565 else if (sRef_isParam (s ) )
572 ct = sRef_getType (s);
573 param = sRef_getParam(s);
575 ctString = ctype_dump(ct);
577 fprintf(f, "Param %s %d\n", cstring_toCharsSafe(ctString), (int) param );
578 cstring_free(ctString);
582 u = sRef_getUentry(s);
583 fprintf(f, "%s\n", cstring_toCharsSafe(uentry_rawName (u) ) );
590 fprintf (f, "%ld\n", t->value.intlit);
600 /*@only@*/ constraintTerm constraintTerm_undump ( FILE *f)
602 constraintTermType kind;
610 os = mstring_create (MAX_DUMP_LINE_LENGTH);
612 str = fgets (os, MAX_DUMP_LINE_LENGTH, f);
614 kind = (constraintTermType) reader_getInt(&str);
615 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
624 term = reader_getWord(&str);
626 if (strcmp (term, "Result") == 0 )
628 s = sRef_makeResult (ctype_unknown);
630 else if (strcmp (term, "Param" ) == 0 )
637 reader_checkChar(&str, ' ');
638 str2 = reader_getWord(&str);
639 param = reader_getInt(&str);
642 t = ctype_undump(&str2) ;
643 s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc));
646 else /* This must be an identified that we can search for in usymTab */
648 cstring termStr = cstring_makeLiteralTemp(term);
650 ue = usymtab_lookup (termStr);
651 s = uentry_getSref(ue);
654 ret = constraintTerm_makesRef(s);
666 term = reader_getWord(&str);
667 /* This must be an identifier that we can search for in usymTab */
668 termStr = cstring_makeLiteralTemp(term);
670 ue = usymtab_lookup (termStr);
671 s = uentry_getSref(ue);
672 ret = constraintTerm_makesRef(s);
683 i = reader_getInt(&str);
684 ret = constraintTerm_makeIntLiteral (i);
698 /* drl added sometime before 10/17/001*/
699 ctype constraintTerm_getCType (constraintTerm term)
706 ct = exprNode_getType (term->value.expr);
711 ct = ctype_signedintegral;
715 ct = sRef_getType (term->value.sref) ;