From: drl7x Date: Mon, 31 Mar 2003 03:29:18 +0000 (+0000) Subject: Committing after merging Evan's changes. X-Git-Tag: splint-3_1_0~28 X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/commitdiff_plain/2a6e9c30f59a18a1f6e678745a79ae5bda5b6a99 Committing after merging Evan's changes. This code breaken but atleast it compile making it an improvement over the current version which doesn't compile after yesterday's committs. --- diff --git a/README b/README index e05b904..af60683 100644 --- a/README +++ b/README @@ -5,8 +5,9 @@ University of Virginia, Massachusetts Institute of Technology - Version 3.0.1.7 - 2 March 20023 + Version 3.0.1.7 + 31 March 2003 + Splint Documentation ==================== diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h index 7133a42..05c7ddf 100644 --- a/src/Headers/constraint.h +++ b/src/Headers/constraint.h @@ -63,12 +63,12 @@ extern /*@only@*/ cstring arithType_print (arithType p_ar) /*@*/; extern /*@only@*/ fileloc constraint_getFileloc (constraint p_c); -extern /*@only@*/ cstring constraint_unparse (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/; -# define constraint_unparse constraint_print +extern /*@only@*/ cstring constraint_unparse (/*@temp@*/ constraint p_c) /*@*/; +extern /*@only@*/ cstring constraint_unparseOr (/*@temp@*/ constraint p_c) /*@*/ ; +extern /*@only@*/ cstring constraint_unparseDetailed (constraint p_c) /*@*/ ; -extern /*@only@*/ cstring constraint_print (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/; - -extern /*@only@*/ constraint constraint_makeWriteSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_po, int p_ind); +extern /*@only@*/ constraint +constraint_makeWriteSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_po, int p_ind); extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode p_dst, exprNode p_src) /*@modifies p_dst @*/; @@ -79,8 +79,6 @@ extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (/*@de extern constraint constraint_preserveOrig (/*@returned@*/ constraint p_c) /*@modifies p_c @*/; extern /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint p_precondition, exprNodeList p_arglist); -extern /*@only@*/ cstring constraint_printDetailed (constraint p_c); - extern /*@only@*/ constraint constraint_makeEnsureLessThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint); extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint); @@ -123,8 +121,6 @@ exprNode_traversEnsuresConstraints (exprNode p_e); extern constraint constraint_togglePost (/*@returned@*/ constraint p_c); extern bool constraint_same (constraint p_c1, constraint p_c2) ; - -/*@only@*/ cstring constraint_printOr (constraint p_c) /*@*/; extern void constraint_printErrorPostCondition (constraint p_c, fileloc p_loc) ; extern cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint p_c) /*@*/; /*drl add 8-11-001*/ diff --git a/src/Headers/constraintList.h b/src/Headers/constraintList.h index 85c2f38..94b190f 100644 --- a/src/Headers/constraintList.h +++ b/src/Headers/constraintList.h @@ -55,12 +55,9 @@ extern constraintList constraintList_copy ( /*@observer@*/ /*@temp@*/ constraint extern void constraintList_free (/*@only@*/ constraintList p_s) ; -extern /*@only@*/ cstring constraintList_unparse ( /*@observer@*/ constraintList p_s) /*@*/; +extern /*@only@*/ cstring constraintList_unparse (/*@observer@*/ constraintList p_s) /*@*/; -/*@only@*/ extern cstring constraintList_print ( /*@observer@*/ /*@temp@*/ constraintList p_s) /*@*/; - -extern cstring -constraintList_printDetailed ( /*@observer@*/ constraintList p_s) /*@*/; +extern cstring constraintList_unparseDetailed (/*@observer@*/ constraintList p_s) /*@*/; extern /*@only@*/ constraintList constraintList_logicalOr ( /*@observer@*/ constraintList p_l1, /*@observer@*/ constraintList p_l2); diff --git a/src/Headers/constraintTerm.h b/src/Headers/constraintTerm.h index 673de12..90d6764 100644 --- a/src/Headers/constraintTerm.h +++ b/src/Headers/constraintTerm.h @@ -9,13 +9,12 @@ typedef union long intlit; } constraintTermValue; -/*@-namechecks@*/ - typedef enum { - ERRORBADCONSTRAINTTERMTYPE, - EXPRNODE, SREF, - INTLITERAL + CTT_ERRORBADCONSTRAINTTERMTYPE, + CTT_EXPR, + CTT_SREF, + CTT_INTLITERAL } constraintTermType; struct _constraintTerm { @@ -50,8 +49,6 @@ fileloc constraintTerm_getFileloc (constraintTerm t) /*@*/; bool constraintTerm_isIntLiteral (constraintTerm term) /*@*/; -cstring constraintTerm_print (constraintTerm term) /*@*/; - constraintTerm constraintTerm_makesRef (/*@temp@*/ /*@observer@*/ sRef s) /*@*/; /*@unused@*/ bool constraintTerm_probSame (constraintTerm term1, constraintTerm term2) /*@*/; @@ -66,31 +63,21 @@ cstring constraintTerm_getStringLiteral (constraintTerm c) /*@*/; constraintTerm constraintTerm_doSRefFixBaseParam (/*@returned@*/ constraintTerm term, exprNodeList arglist) /*@modifies term@*/; -void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f); - -/*@only@*/ constraintTerm constraintTerm_undump ( FILE *f); - -bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm p_c) /*@*/; - -int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm p_c) /*@*/; - -bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/; - +extern cstring constraintTerm_unparse (constraintTerm) /*@*/ ; +extern void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f); +extern /*@only@*/ constraintTerm constraintTerm_undump ( FILE *f); +extern bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm p_c) /*@*/; +extern int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm p_c) /*@*/; +extern bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/; extern ctype constraintTerm_getCType (constraintTerm term); -/*@exposed@*/ exprNode constraintTerm_getExprNode (constraintTerm t); - -/*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t); - - -/*@=namechecks@*/ +extern /*@exposed@*/ exprNode constraintTerm_getExprNode (constraintTerm t); +extern /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t); /*drl added 12/19/2002*/ -bool constraintTerm_isConstantOnly ( constraintTerm p_term ); +extern bool constraintTerm_isConstantOnly (constraintTerm p_term); #else - -#error Multiple Include - +#error "Multiple Include!" #endif diff --git a/src/Headers/ltoken.h b/src/Headers/ltoken.h index 7b7b68b..78c994f 100644 --- a/src/Headers/ltoken.h +++ b/src/Headers/ltoken.h @@ -107,7 +107,7 @@ extern bool ltoken_wasSyn (/*@sef@*/ ltoken p_tok); # define ltoken_wasSyn(tok) \ (ltoken_isValid (tok) ? lsymbol_isDefined ((tok)->rawText) : FALSE) -/*@-namechecks@*/ +/*@-namechecks@*/ /* all of these should start with g_ */ extern /*@dependent@*/ ltoken ltoken_forall; extern /*@dependent@*/ ltoken ltoken_exists; extern /*@dependent@*/ ltoken ltoken_true; diff --git a/src/Headers/sort.h b/src/Headers/sort.h index 8e2073b..9540a76 100644 --- a/src/Headers/sort.h +++ b/src/Headers/sort.h @@ -160,15 +160,13 @@ extern sort sort_fromLsymbol (lsymbol p_sortid) /*@modifies internalState@*/ ; extern void sort_import (inputStream p_imported, ltoken p_tok, mapping p_map) /*@modifies p_imported, internalState@*/ ; -/*@-namechecks@*/ -extern sort sort_bool; -extern sort sort_capBool; -extern sort sort_int; -extern sort sort_char; -extern sort sort_cstring; -extern sort sort_float; -extern sort sort_double; -/*@=namechecks@*/ +extern sort g_sortBool; +extern sort g_sortCapBool; +extern sort g_sortInt; +extern sort g_sortChar; +extern sort g_sortCstring; +extern sort g_sortFloat; +extern sort g_sortDouble; # else # error "Multiple include" diff --git a/src/Makefile.am b/src/Makefile.am index d486f22..b4a45f6 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -393,10 +393,10 @@ etags: lintnew: splintme splintme: - ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw + ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw -splintmenosupcounts: - ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw +splintmesupcounts: + ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -supcounts -constuse -mts file -mts filerw lintbuffercheck: ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(LINTSRC) $(OVERFLOWCHSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw +bounds -DLINTBUFFERCHECK diff --git a/src/Makefile.in b/src/Makefile.in index 8ac5db3..103e7b1 100644 --- a/src/Makefile.in +++ b/src/Makefile.in @@ -1124,10 +1124,10 @@ etags: lintnew: splintme splintme: - ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw + ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw -splintmenosupcounts: - ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw +splintmesupcounts: + ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -supcounts -constuse -mts file -mts filerw lintbuffercheck: ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(LINTSRC) $(OVERFLOWCHSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw +bounds -DLINTBUFFERCHECK diff --git a/src/abstract.c b/src/abstract.c index 62f8994..3e95eae 100644 --- a/src/abstract.c +++ b/src/abstract.c @@ -186,7 +186,7 @@ abstract_init () ti->modifiable = FALSE; ti->abstract = FALSE; ti->export = FALSE; /* this is implicit, not exported */ - ti->basedOn = sort_float; + ti->basedOn = g_sortFloat; symtable_enterType (g_symtab, ti); } @@ -236,7 +236,7 @@ void LCLBuiltins (void) ti->modifiable = FALSE; ti->abstract = TRUE; - ti->basedOn = sort_bool; + ti->basedOn = g_sortBool; ti->export = FALSE; /* this wasn't set (detected by Splint) */ symtable_enterType (g_symtab, ti); @@ -244,7 +244,7 @@ void LCLBuiltins (void) vi->id = ltoken_createType (simpleId, SID_VAR, lsymbol_fromChars ("FALSE")); vi->kind = VRK_CONST; - vi->sort = sort_bool; + vi->sort = g_sortBool; vi->export = TRUE; (void) symtable_enterVar (g_symtab, vi); @@ -3701,7 +3701,7 @@ makeQuantifiedTermNode (quantifierNodeList qn, ltoken open, termNodeList_free (t->args); t->args = termNodeList_new (); - sort = sort_bool; + sort = g_sortBool; n->sort = sort; (void) sortSet_insert (n->possibleSorts, sort); @@ -4223,7 +4223,7 @@ makeLiteralTermNode (ltoken tok, sort s) needed anyway. */ /* symtable_enterOp (g_symtab, nn, sign); */ - if (s == sort_int) + if (s == g_sortInt) { sigNode osign; lslOp opn = (lslOp) dmalloc (sizeof (*opn)); @@ -4231,7 +4231,7 @@ makeLiteralTermNode (ltoken tok, sort s) /* if it is a C int, we should overload it as double too because C allows you to say "x > 2". */ - (void) sortSet_insert (n->possibleSorts, sort_double); + (void) sortSet_insert (n->possibleSorts, g_sortDouble); ltoken_setText (range, lsymbol_fromChars ("double")); osign = makesigNode (ltoken_undefined, ltokenList_new (), range); @@ -4261,7 +4261,7 @@ makeUnchangedTermNode1 (ltoken op, /*@unused@*/ ltoken all) t->error_reported = FALSE; t->wrapped = 0; t->kind = TRM_UNCHANGEDALL; - t->sort = sort_bool; + t->sort = g_sortBool; t->literal = op; t->given = sort_makeNoSort (); t->name = NULL; /*< missing this >*/ @@ -4286,7 +4286,7 @@ makeUnchangedTermNode2 (ltoken op, storeRefNodeList x) t->error_reported = FALSE; t->wrapped = 0; t->kind = TRM_UNCHANGEDOTHERS; - t->sort = sort_bool; + t->sort = g_sortBool; t->literal = op; t->unchanged = x; t->given = sort_makeNoSort (); @@ -4338,7 +4338,7 @@ makeUnchangedTermNode2 (ltoken op, storeRefNodeList x) t->error_reported = FALSE; t->wrapped = 0; t->kind = TRM_SIZEOF; - t->sort = sort_int; + t->sort = g_sortInt; t->literal = op; t->sizeofField = type; t->given = sort_makeNoSort (); diff --git a/src/checking.c b/src/checking.c index 7adb6db..7e11ce8 100644 --- a/src/checking.c +++ b/src/checking.c @@ -398,7 +398,7 @@ checkLclPredicate (ltoken t, lclPredicateNode n) { /* check that the sort of n is boolean */ theSort = n->predicate->sort; - if (!sort_compatible (theSort, sort_capBool)) + if (!sort_compatible (theSort, g_sortCapBool)) { if (sort_isNoSort (theSort)) { @@ -582,14 +582,14 @@ standardOperators (/*@null@*/ nameNode n, sortSetList argSorts, /*@unused@*/ sor { if (sn->kind == SRT_OBJ || sn->kind == SRT_ARRAY) - (void) sortSet_insert (ret, sort_bool); + (void) sortSet_insert (ret, g_sortBool); } if (cstring_equalLit (text, "maxIndex") || cstring_equalLit (text, "minIndex")) { if (sn->kind == SRT_ARRAY || sn->kind == SRT_PTR) - (void) sortSet_insert (ret, sort_int); + (void) sortSet_insert (ret, g_sortInt); /* if (lsymbol_fromChars ("maxIndex") */ } @@ -601,14 +601,14 @@ standardOperators (/*@null@*/ nameNode n, sortSetList argSorts, /*@unused@*/ sor if (sn->kind == SRT_OBJ || sn->kind == SRT_ARRAY) { - (void) sortSet_insert (ret, sort_bool); + (void) sortSet_insert (ret, g_sortBool); } break; case LLT_SIZEOF: if (sn->kind == SRT_OBJ || sn->kind == SRT_ARRAY || sn->kind == SRT_VECTOR) - (void) sortSet_insert (ret, sort_int); + (void) sortSet_insert (ret, g_sortInt); break; default: break; @@ -634,7 +634,7 @@ standardOperators (/*@null@*/ nameNode n, sortSetList argSorts, /*@unused@*/ sor { argSet = sortSetList_head (argSorts); - if (sortSet_member (argSet, sort_bool)) + if (sortSet_member (argSet, g_sortBool)) { sortSetList_reset (argSorts); sortSetList_advance (argSorts); @@ -778,7 +778,7 @@ standardOperators (/*@null@*/ nameNode n, sortSetList argSorts, /*@unused@*/ sor { if (sort_equal (cl, cl2)) { - (void) sortSet_insert (ret, sort_bool); + (void) sortSet_insert (ret, g_sortBool); } } end_sortSet_elements; } end_sortSet_elements; diff --git a/src/constraint.c b/src/constraint.c index fe7b638..0d39b6e 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -28,17 +28,15 @@ /* #define DEBUGPRINT 1 */ -# include /* for isdigit */ # include "splintMacros.nf" # include "basic.h" # include "cgrammar.h" # include "cgrammar_tokens.h" - # include "exprChecks.h" # include "exprNodeSList.h" - -static /*@only@*/ cstring constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c); +static /*@only@*/ cstring +constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c); static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void) /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/ @@ -50,39 +48,6 @@ advanceField (char **s) reader_checkChar (s, '@'); } -# if 0 -static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant) -{ - char *t; - int c; - constraint ret; - ret = constraint_makeNew (); - llassert (constraintExpr_isDefined (l)); - - ret->lexpr = constraintExpr_copy (l); - - - if (relOp.tok == GE_OP) - ret->ar = GTE; - else if (relOp.tok == LE_OP) - ret->ar = LTE; - else if (relOp.tok == EQ_OP) - ret->ar = EQ; - else - llfatalbug (message ("Unsupported relational operator")); - - - t = cstring_toCharsSafe (exprNode_unparse (cconstant)); - c = atoi ( t); - ret->expr = constraintExpr_makeIntLiteral (c); - - ret->post = TRUE; - DPRINTF (("GENERATED CONSTRAINT:")); - DPRINTF ((message ("%s", constraint_unparse (ret)))); - return ret; -} -# endif - bool constraint_same (constraint c1, constraint c2) { llassert (c1 != NULL); @@ -348,7 +313,6 @@ constraint constraint_makeReadSafeExprNode (exprNode po, exprNode ind) constraint constraint_makeWriteSafeInt ( exprNode po, int ind) { constraint ret = constraint_makeNew (); - ret->lexpr =constraintExpr_makeMaxSetExpr (po); ret->ar = GTE; diff --git a/src/constraintExpr.c b/src/constraintExpr.c index 5ea57e0..7093b6e 100644 --- a/src/constraintExpr.c +++ b/src/constraintExpr.c @@ -1888,25 +1888,23 @@ doFixResultTerm (/*@only@*/ constraintExpr e, /*@exposed@*/ exprNode fcnCall) { constraintTerm t; sRef s; - - constraintExprData data; constraintExprKind kind; - constraintExpr ret; - - llassert(constraintExpr_isDefined (e) ); + + llassert (constraintExpr_isDefined (e) ); data = e->data; kind = e->kind; - - llassert(kind == term); - + + llassert (kind == term); + t = constraintExprData_termGetTerm (data); - llassert (constraintTerm_isDefined(t) ); - + llassert (constraintTerm_isDefined (t)); + ret = e; - switch (constraintTerm_getKind(t) ) + + switch (constraintTerm_getKind (t)) { case CTT_EXPR: case CTT_INTLITERAL: @@ -1932,7 +1930,11 @@ doFixResultTerm (/*@only@*/ constraintExpr e, /*@exposed@*/ exprNode fcnCall) return ret; } -/* + +#if 0 + +/*to be used for structure checking */ + / *@only@* / static constraintExpr doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e, sRef s, ctype ct) @@ -1991,7 +1993,7 @@ doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e, return ret; } -*/ +#endif /*drl moved from constriantTerm.c 5/20/001*/ /*@only@*/ static constraintExpr diff --git a/src/constraintList.c b/src/constraintList.c index 625d716..24654bc 100644 --- a/src/constraintList.c +++ b/src/constraintList.c @@ -278,7 +278,7 @@ constraintList_unparse (/*@temp@*/ constraintList s) /*@*/ if (context_getFlag (FLG_ORCONSTRAINT)) { - temp1 = constraint_unparseOr(current); + temp1 = constraint_unparseOr (current); } else { @@ -301,7 +301,7 @@ constraintList_unparse (/*@temp@*/ constraintList s) /*@*/ return st; } -void constraintList_unparseErrorPostConditions (constraintList s, fileloc loc) +void constraintList_printErrorPostConditions (constraintList s, fileloc loc) { constraintList_elements (s, elem) @@ -315,7 +315,7 @@ void constraintList_unparseErrorPostConditions (constraintList s, fileloc loc) return; } -void constraintList_unparseError (constraintList s, fileloc loc) +void constraintList_printError (constraintList s, fileloc loc) { constraintList_elements (s, elem) diff --git a/src/constraintTerm.c b/src/constraintTerm.c index 8c4ce96..807a0bd 100644 --- a/src/constraintTerm.c +++ b/src/constraintTerm.c @@ -50,23 +50,23 @@ void constraintTerm_free (/*@only@*/ constraintTerm term) switch (term->kind) { - case EXPRNODE: + case CTT_EXPR: /* we don't free an exprNode*/ break; - case SREF: + case CTT_SREF: /* sref */ sRef_free (term->value.sref); break; - case INTLITERAL: + case CTT_INTLITERAL: /* don't free an int */ break; - case ERRORBADCONSTRAINTTERMTYPE: + case CTT_ERRORBADCONSTRAINTTERMTYPE: default: /* type was set incorrectly */ llcontbug (message("constraintTerm_free type was set incorrectly")); } - term->kind = ERRORBADCONSTRAINTTERMTYPE; + term->kind = CTT_ERRORBADCONSTRAINTTERMTYPE; free (term); } @@ -83,7 +83,7 @@ bool constraintTerm_isIntLiteral (constraintTerm term) { llassert(term != NULL); - if (term->kind == INTLITERAL) + if (term->kind == CTT_INTLITERAL) return TRUE; return FALSE; @@ -93,10 +93,10 @@ bool constraintTerm_isIntLiteral (constraintTerm term) bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/ { llassert (c != NULL); - if (c->kind == EXPRNODE) + + if (c->kind == CTT_EXPR) { - - if (exprNode_isInitBlock(c->value.expr) ) + if (exprNode_isInitBlock (c->value.expr)) { return TRUE; } @@ -108,7 +108,8 @@ bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@ bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/ { llassert (c != NULL); - if (c->kind == EXPRNODE) + + if (c->kind == CTT_EXPR) { return TRUE; } @@ -118,12 +119,11 @@ bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@* /*@access exprNode@*/ int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/ { - - exprNodeList list; + exprNodeList list; int ret; llassert (c != NULL); llassert (constraintTerm_isInitBlock (c) ); - llassert (c->kind == EXPRNODE); + llassert (c->kind == CTT_EXPR); llassert(exprNode_isDefined(c->value.expr) ); @@ -148,7 +148,7 @@ int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm bool constraintTerm_isStringLiteral (constraintTerm c) /*@*/ { llassert (c != NULL); - if (c->kind == EXPRNODE) + if (c->kind == CTT_EXPR) { if (exprNode_knownStringValue(c->value.expr) ) { @@ -164,14 +164,14 @@ cstring constraintTerm_getStringLiteral (constraintTerm c) { llassert (c != NULL); llassert (constraintTerm_isStringLiteral (c) ); - llassert (c->kind == EXPRNODE); + llassert (c->kind == CTT_EXPR); return (cstring_copy ( multiVal_forceString (exprNode_getValue (c->value.expr) ) ) ); } constraintTerm constraintTerm_simplify (/*@returned@*/ constraintTerm term) /*@modifies term@*/ { - if (term->kind == EXPRNODE) + if (term->kind == CTT_EXPR) { if ( exprNode_knownIntValue (term->value.expr ) ) { @@ -179,7 +179,7 @@ constraintTerm constraintTerm_simplify (/*@returned@*/ constraintTerm term) /*@m temp = exprNode_getLongValue (term->value.expr); term->value.intlit = (int)temp; - term->kind = INTLITERAL; + term->kind = CTT_INTLITERAL; } } return term; @@ -201,7 +201,7 @@ constraintTermType constraintTerm_getKind (constraintTerm t) /*@exposed@*/ sRef constraintTerm_getSRef (constraintTerm t) { llassert (constraintTerm_isDefined(t) ); - llassert (t->kind == SREF); + llassert (t->kind == CTT_SREF); return (t->value.sref); } @@ -211,7 +211,7 @@ constraintTermType constraintTerm_getKind (constraintTerm t) constraintTerm ret = new_constraintTermExpr(); ret->loc = fileloc_copy(exprNode_getfileloc(e)); ret->value.expr = e; - ret->kind = EXPRNODE; + ret->kind = CTT_EXPR; ret = constraintTerm_simplify(ret); return ret; } @@ -221,7 +221,7 @@ constraintTermType constraintTerm_getKind (constraintTerm t) constraintTerm ret = new_constraintTermExpr(); ret->loc = fileloc_undefined; ret->value.sref = sRef_saveCopy(s); - ret->kind = SREF; + ret->kind = CTT_SREF; ret = constraintTerm_simplify(ret); return ret; } @@ -236,14 +236,14 @@ constraintTerm constraintTerm_copy (constraintTerm term) switch (term->kind) { - case EXPRNODE: + case CTT_EXPR: ret->value.expr = term->value.expr; break; - case INTLITERAL: + case CTT_INTLITERAL: ret->value.intlit = term->value.intlit; break; - case SREF: + case CTT_SREF: ret->value.sref = sRef_saveCopy(term->value.sref); break; default: @@ -274,15 +274,15 @@ static cstring constraintTerm_getName (constraintTerm term) switch (term->kind) { - case EXPRNODE: + case CTT_EXPR: s = message ("%s", exprNode_unparse (term->value.expr) ); break; - case INTLITERAL: + case CTT_INTLITERAL: s = message (" %d ", (int) term->value.intlit); break; - case SREF: + case CTT_SREF: s = message ("%q", sRef_unparse (term->value.sref) ); break; @@ -302,13 +302,13 @@ constraintTerm_doSRefFixBaseParam (/*@returned@*/constraintTerm term, exprNodeLi switch (term->kind) { - case EXPRNODE: + case CTT_EXPR: break; - case INTLITERAL: + case CTT_INTLITERAL: break; - case SREF: + case CTT_SREF: term->value.sref = sRef_fixBaseParam (term->value.sref, arglist); break; default: @@ -318,7 +318,7 @@ constraintTerm_doSRefFixBaseParam (/*@returned@*/constraintTerm term, exprNodeLi } -cstring constraintTerm_print (constraintTerm term) /*@*/ +cstring constraintTerm_unparse (constraintTerm term) /*@*/ { cstring s; s = cstring_undefined; @@ -327,16 +327,16 @@ cstring constraintTerm_print (constraintTerm term) /*@*/ switch (term->kind) { - case EXPRNODE: + case CTT_EXPR: s = message ("%s @ %q", exprNode_unparse (term->value.expr), fileloc_unparse (term->loc) ); break; - case INTLITERAL: + case CTT_INTLITERAL: s = message ("%d", (int)term->value.intlit); break; - case SREF: + case CTT_SREF: s = message ("%q", sRef_unparseDebug (term->value.sref) ); break; @@ -352,18 +352,18 @@ constraintTerm constraintTerm_makeIntLiteral (long i) { constraintTerm ret = new_constraintTermExpr(); ret->value.intlit = i; - ret->kind = INTLITERAL; + ret->kind = CTT_INTLITERAL; ret->loc = fileloc_undefined; return ret; } bool constraintTerm_canGetValue (constraintTerm term) { - if (term->kind == INTLITERAL) + if (term->kind == CTT_INTLITERAL) { return TRUE; } - else if (term->kind == SREF) + else if (term->kind == CTT_SREF) { if (sRef_hasValue (term->value.sref)) { @@ -376,7 +376,7 @@ bool constraintTerm_canGetValue (constraintTerm term) return FALSE; } } - else if (term->kind == EXPRNODE) + else if (term->kind == CTT_EXPR) { return FALSE; } @@ -390,11 +390,11 @@ long constraintTerm_getValue (constraintTerm term) { llassert (constraintTerm_canGetValue (term)); - if (term->kind == INTLITERAL) + if (term->kind == CTT_INTLITERAL) { return term->value.intlit; } - else if (term->kind == SREF) + else if (term->kind == CTT_SREF) { if (sRef_hasValue (term->value.sref)) { @@ -407,7 +407,7 @@ long constraintTerm_getValue (constraintTerm term) BADBRANCH; } } - else if (term->kind == EXPRNODE) + else if (term->kind == CTT_EXPR) { BADBRANCH; } @@ -426,7 +426,7 @@ long constraintTerm_getValue (constraintTerm term) { llassert (t != NULL); - llassert (t->kind == EXPRNODE); + llassert (t->kind == CTT_EXPR); return t->value.expr; @@ -435,12 +435,12 @@ long constraintTerm_getValue (constraintTerm term) /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t) { llassert (t != NULL); - if (t->kind == EXPRNODE) + if (t->kind == CTT_EXPR) { return exprNode_getSref(t->value.expr); } - if (t->kind == SREF) + if (t->kind == CTT_SREF) { return t->value.sref; } @@ -482,7 +482,9 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) llassert (term1 !=NULL && term2 !=NULL); if (constraintTerm_canGetValue (term1) && constraintTerm_canGetValue (term2)) - /* evans 2001-07-24: was (term1->kind == INTLITERAL) && (term2->kind == INTLITERAL) ) */ + + /*3/30/2003 comment updated to reflect name change form INTLITERAL to CTT_INTLITERAL*/ + /* evans 2001-07-24: was (term1->kind == CTT_INTLITERAL) && (term2->kind == CTT_INTLITERAL) ) */ { long t1, t2; @@ -542,12 +544,12 @@ void constraintTerm_dump (/*@observer@*/ constraintTerm t, FILE *f) switch (kind) { - case EXPRNODE: + case CTT_EXPR: u = exprNode_getUentry(t->value.expr); fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u))); break; - case SREF: + case CTT_SREF: { sRef s; @@ -585,7 +587,7 @@ void constraintTerm_dump (/*@observer@*/ constraintTerm t, FILE *f) } break; - case INTLITERAL: + case CTT_INTLITERAL: fprintf (f, "%ld\n", t->value.intlit); break; @@ -620,7 +622,7 @@ void constraintTerm_dump (/*@observer@*/ constraintTerm t, FILE *f) switch (kind) { - case SREF: + case CTT_SREF: { sRef s; char * term; @@ -674,7 +676,7 @@ void constraintTerm_dump (/*@observer@*/ constraintTerm t, FILE *f) } break; - case EXPRNODE: + case CTT_EXPR: { sRef s; char * term; @@ -699,7 +701,7 @@ void constraintTerm_dump (/*@observer@*/ constraintTerm t, FILE *f) break; - case INTLITERAL: + case CTT_INTLITERAL: { int i; @@ -725,16 +727,16 @@ ctype constraintTerm_getCType (constraintTerm term) switch (term->kind) { - case EXPRNODE: + case CTT_EXPR: ct = exprNode_getType (term->value.expr); break; - case INTLITERAL: + case CTT_INTLITERAL: /*@i888*/ /* hack */ ct = ctype_signedintegral; break; - case SREF: + case CTT_SREF: ct = sRef_getType (term->value.sref) ; break; default: @@ -747,7 +749,7 @@ bool constraintTerm_isConstantOnly (constraintTerm term) { switch (term->kind) { - case EXPRNODE: + case CTT_EXPR: if (exprNode_isNumLiteral (term->value.expr) || exprNode_isStringLiteral (term->value.expr) || exprNode_isCharLiteral (term->value.expr) ) @@ -759,10 +761,10 @@ bool constraintTerm_isConstantOnly (constraintTerm term) return FALSE; } - case INTLITERAL: + case CTT_INTLITERAL: return TRUE; - case SREF: + case CTT_SREF: if ( sRef_isConst (term->value.sref) ) { return TRUE; diff --git a/src/imports.c b/src/imports.c index 55c937b..bc91fe9 100644 --- a/src/imports.c +++ b/src/imports.c @@ -124,7 +124,7 @@ importCTrait (void) callLSL (cstring_makeLiteralTemp (CTRAITSPECNAME), message ("includes %s (%s for String)", cstring_fromChars (CTRAITFILENAMEN), - cstring_fromChars (sort_getName (sort_cstring)))); + cstring_fromChars (sort_getName (g_sortCstring)))); cstring_free (infile); break; } diff --git a/src/llgrammar.c.der b/src/llgrammar.c.der index 1dc52a1..2ce2282 100644 --- a/src/llgrammar.c.der +++ b/src/llgrammar.c.der @@ -3441,16 +3441,16 @@ case 392: { yyval.term = makeSizeofTermNode (yyvsp[-3].ltok, yyvsp[-1].lcltypespec); ; break;} case 393: -{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, sort_int); ; +{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, g_sortInt); ; break;} case 394: -{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, sort_cstring); ; +{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, g_sortCstring); ; break;} case 395: -{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, sort_char); ; +{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, g_sortChar); ; break;} case 396: -{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, sort_double); ; +{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, g_sortDouble); ; break;} case 397: { yyval.quantifiers = quantifierNodeList_add (quantifierNodeList_new (), yyvsp[0].quantifier); ; diff --git a/src/llgrammar.y b/src/llgrammar.y index e83c598..ab30d80 100644 --- a/src/llgrammar.y +++ b/src/llgrammar.y @@ -1361,10 +1361,10 @@ lclPrimary */ cLiteral - : LLT_CINTEGER { $$ = makeLiteralTermNode ($1, sort_int); } - | LLT_LCSTRING { $$ = makeLiteralTermNode ($1, sort_cstring); } - | LLT_CCHAR { $$ = makeLiteralTermNode ($1, sort_char); } - | LLT_CFLOAT { $$ = makeLiteralTermNode ($1, sort_double); } + : LLT_CINTEGER { $$ = makeLiteralTermNode ($1, g_sortInt); } + | LLT_LCSTRING { $$ = makeLiteralTermNode ($1, g_sortCstring); } + | LLT_CCHAR { $$ = makeLiteralTermNode ($1, g_sortChar); } + | LLT_CFLOAT { $$ = makeLiteralTermNode ($1, g_sortDouble); } ; quantifiers diff --git a/src/ltoken.c b/src/ltoken.c index 8136819..cc6e383 100644 --- a/src/ltoken.c +++ b/src/ltoken.c @@ -37,7 +37,7 @@ ** set in LCLScanLineInit of lclscanline.c or in scanline.c */ -/*@-namechecks@*/ +/*@-namechecks@*/ /* These should all start with g_ */ ltoken ltoken_forall; ltoken ltoken_exists; ltoken ltoken_true; diff --git a/src/sort.c b/src/sort.c index 1196738..e8266ed 100644 --- a/src/sort.c +++ b/src/sort.c @@ -110,15 +110,13 @@ static /*@only@*/ nameNode makeArrowFieldOp (lsymbol p_field); static lsymbol sp (lsymbol p_s1, lsymbol p_s2); static void sortError (ltoken p_t, sort p_oldsort, sortNode p_newnode); -/*@-namechecks@*/ -sort sort_bool; -sort sort_capBool; -sort sort_int; -sort sort_char; -sort sort_float; -sort sort_double; -sort sort_cstring; -/*@=namechecks@*/ +sort g_sortBool; +sort g_sortCapBool; +sort g_sortInt; +sort g_sortChar; +sort g_sortFloat; +sort g_sortDouble; +sort g_sortCstring; static sort sort_void; static sort char_obj_ptrSort; @@ -1909,31 +1907,31 @@ sort_init (void) /* Other builtin sorts */ - sort_bool = sort_makeImmutable (ltoken_undefined, lsymbol_fromChars ("bool")); - sort_capBool = sort_makeSortNoOps (ltoken_undefined, lsymbol_fromChars ("Bool")); + g_sortBool = sort_makeImmutable (ltoken_undefined, lsymbol_fromChars ("bool")); + g_sortCapBool = sort_makeSortNoOps (ltoken_undefined, lsymbol_fromChars ("Bool")); llassert (sortTable != NULL); - /* make sort_Bool a synonym for sort_bool */ - sortTable[sort_capBool]->kind = SRT_SYN; - sortTable[sort_capBool]->baseSort = sort_bool; - sortTable[sort_capBool]->mutable = FALSE; - sortTable[sort_capBool]->abstract = TRUE; + /* make g_sortBool a synonym for g_sortBool */ + sortTable[g_sortCapBool]->kind = SRT_SYN; + sortTable[g_sortCapBool]->baseSort = g_sortBool; + sortTable[g_sortCapBool]->mutable = FALSE; + sortTable[g_sortCapBool]->abstract = TRUE; - sort_int = sort_makeLiteralSort (ltoken_undefined, + g_sortInt = sort_makeLiteralSort (ltoken_undefined, lsymbol_fromChars ("int")); - sort_char = sort_makeLiteralSort (ltoken_undefined, + g_sortChar = sort_makeLiteralSort (ltoken_undefined, lsymbol_fromChars ("char")); sort_void = sort_makeLiteralSort (ltoken_undefined, lsymbol_fromChars ("void")); - /* sort_cstring is char__Vec, for C strings eg: "xyz" */ - char_obj_ptrSort = sort_makePtr (ltoken_undefined, sort_char); - char_obj_ArrSort = sort_makeArr (ltoken_undefined, sort_char); + /* g_sortCstring is char__Vec, for C strings eg: "xyz" */ + char_obj_ptrSort = sort_makePtr (ltoken_undefined, g_sortChar); + char_obj_ArrSort = sort_makeArr (ltoken_undefined, g_sortChar); - sort_cstring = sort_makeVal (char_obj_ArrSort); - sort_float = sort_makeLiteralSort (ltoken_undefined, lsymbol_fromChars ("float")); - sort_double = sort_makeLiteralSort (ltoken_undefined, lsymbol_fromChars ("double")); + g_sortCstring = sort_makeVal (char_obj_ArrSort); + g_sortFloat = sort_makeLiteralSort (ltoken_undefined, lsymbol_fromChars ("float")); + g_sortDouble = sort_makeLiteralSort (ltoken_undefined, lsymbol_fromChars ("double")); } sort @@ -3082,7 +3080,7 @@ sort_compatible_modulo_cstring (sort s1, sort s2) return TRUE; syn1 = sort_getUnderlying (s1); syn2 = sort_getUnderlying (s2); - if (sort_cstring == syn2 && + if (g_sortCstring == syn2 && (syn1 == char_obj_ptrSort || syn1 == char_obj_ArrSort)) return TRUE; return FALSE;