X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/bb7c2085a0088f4a6b3fb68dcd0ce331f67e9a2d..16c024b587f5ddc115928d5cca7095508aa208d9:/src/constraintTerm.c diff --git a/src/constraintTerm.c b/src/constraintTerm.c index fd19785..e49f75d 100644 --- a/src/constraintTerm.c +++ b/src/constraintTerm.c @@ -17,8 +17,8 @@ ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, ** MA 02111-1307, USA. ** -** For information on lclint: lclint-request@cs.virginia.edu -** To report a bug: lclint-bug@cs.virginia.edu +** For information on splint: info@splint.org +** To report a bug: splint-bug@splint.org ** For more information: http://www.splint.org */ @@ -29,7 +29,7 @@ /* #define DEBUGPRINT 1 */ # include /* for isdigit */ -# include "lclintMacros.nf" +# include "splintMacros.nf" # include "basic.h" # include "cgrammar.h" # include "cgrammar_tokens.h" @@ -38,8 +38,12 @@ # include "exprNodeSList.h" /*@-czechfcns@*/ +/*@-nullderef@*/ /* !!! DRL needs to fix this code! */ +/*@-nullstate@*/ /* !!! DRL needs to fix this code! */ +/*@-nullpass@*/ /* !!! DRL needs to fix this code! */ +/*@-temptrans@*/ /* !!! DRL needs to fix this code! */ -/*@access exprNode @*/ +/*@access exprNode@*/ /* !!! NO! Don't do this recklessly! */ bool constraintTerm_isDefined (constraintTerm t) { @@ -528,7 +532,7 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) } } -void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) +void constraintTerm_dump (/*@observer@*/ constraintTerm t, FILE *f) { fileloc loc; constraintTermValue value; @@ -548,8 +552,7 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) case EXPRNODE: u = exprNode_getUentry(t->value.expr); - fprintf(f, "%s\n", cstring_toCharsSafe( uentry_rawName (u) ) - ); + fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u))); break; case SREF: @@ -562,7 +565,7 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) { fprintf(f, "Result\n"); } - else if (sRef_isParam (s ) ) + else if (sRef_isParam (s)) { int param; ctype ct; @@ -577,10 +580,14 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) fprintf(f, "Param %s %d\n", cstring_toCharsSafe(ctString), (int) param ); cstring_free(ctString); } + else if (sRef_isField (s) ) + { + fprintf(f, "sRef_dump %s\n", cstring_toCharsSafe(sRef_dump(s)) ); + } else { u = sRef_getUentry(s); - fprintf(f, "%s\n", cstring_toCharsSafe(uentry_rawName (u) ) ); + fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u))); } } @@ -597,7 +604,7 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) } -/*@only@*/ constraintTerm constraintTerm_undump ( FILE *f) +/*@only@*/ constraintTerm constraintTerm_undump (FILE *f) { constraintTermType kind; constraintTerm ret; @@ -611,9 +618,13 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) str = fgets (os, MAX_DUMP_LINE_LENGTH, f); + llassert (str != NULL); + kind = (constraintTermType) reader_getInt(&str); str = fgets(os, MAX_DUMP_LINE_LENGTH, f); + llassert (str != NULL); + switch (kind) { @@ -640,9 +651,14 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) ostr2 = str2; t = ctype_undump(&str2) ; - s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc)); + s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc, SA_CREATED)); free (ostr2); } + else if (strcmp (term, "sRef_dump" ) == 0 ) + { + reader_checkChar(&str, ' '); + s = sRef_undump (&str); + } else /* This must be an identified that we can search for in usymTab */ { cstring termStr = cstring_makeLiteralTemp(term); @@ -695,4 +711,28 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) +/* drl added sometime before 10/17/001*/ +ctype constraintTerm_getCType (constraintTerm term) +{ + ctype ct; + + switch (term->kind) + { + case EXPRNODE: + ct = exprNode_getType (term->value.expr); + break; + + case INTLITERAL: + /*@i888*/ /* hack */ + ct = ctype_signedintegral; + break; + + case SREF: + ct = sRef_getType (term->value.sref) ; + break; + default: + BADEXIT; + } + return ct; +}