This code breaken but atleast it compile making it an improvement over the current version which doesn't compile after yesterday's committs.
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
====================
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 @*/;
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);
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*/
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);
long intlit;
} constraintTermValue;
-/*@-namechecks@*/
-
typedef enum
{
- ERRORBADCONSTRAINTTERMTYPE,
- EXPRNODE, SREF,
- INTLITERAL
+ CTT_ERRORBADCONSTRAINTTERMTYPE,
+ CTT_EXPR,
+ CTT_SREF,
+ CTT_INTLITERAL
} constraintTermType;
struct _constraintTerm {
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) /*@*/;
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
# 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;
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"
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
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
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);
}
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);
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);
termNodeList_free (t->args);
t->args = termNodeList_new ();
- sort = sort_bool;
+ sort = g_sortBool;
n->sort = sort;
(void) sortSet_insert (n->possibleSorts, sort);
needed anyway. */
/* symtable_enterOp (g_symtab, nn, sign); */
- if (s == sort_int)
+ if (s == g_sortInt)
{
sigNode osign;
lslOp opn = (lslOp) dmalloc (sizeof (*opn));
/* 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);
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 >*/
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 ();
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 ();
{
/* 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))
{
{
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") */
}
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;
{
argSet = sortSetList_head (argSorts);
- if (sortSet_member (argSet, sort_bool))
+ if (sortSet_member (argSet, g_sortBool))
{
sortSetList_reset (argSorts);
sortSetList_advance (argSorts);
{
if (sort_equal (cl, cl2))
{
- (void) sortSet_insert (ret, sort_bool);
+ (void) sortSet_insert (ret, g_sortBool);
}
} end_sortSet_elements;
} end_sortSet_elements;
/* #define DEBUGPRINT 1 */
-# include <ctype.h> /* 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 @*/
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);
constraint constraint_makeWriteSafeInt ( exprNode po, int ind)
{
constraint ret = constraint_makeNew ();
-
ret->lexpr =constraintExpr_makeMaxSetExpr (po);
ret->ar = GTE;
{
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:
return ret;
}
-/*
+
+#if 0
+
+/*to be used for structure checking */
+
/ *@only@* / static constraintExpr
doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e,
sRef s, ctype ct)
return ret;
}
-*/
+#endif
/*drl moved from constriantTerm.c 5/20/001*/
/*@only@*/ static constraintExpr
if (context_getFlag (FLG_ORCONSTRAINT))
{
- temp1 = constraint_unparseOr(current);
+ temp1 = constraint_unparseOr (current);
}
else
{
return st;
}
-void constraintList_unparseErrorPostConditions (constraintList s, fileloc loc)
+void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
{
constraintList_elements (s, elem)
return;
}
-void constraintList_unparseError (constraintList s, fileloc loc)
+void constraintList_printError (constraintList s, fileloc loc)
{
constraintList_elements (s, elem)
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);
}
{
llassert(term != NULL);
- if (term->kind == INTLITERAL)
+ if (term->kind == CTT_INTLITERAL)
return TRUE;
return FALSE;
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;
}
bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
{
llassert (c != NULL);
- if (c->kind == EXPRNODE)
+
+ if (c->kind == CTT_EXPR)
{
return TRUE;
}
/*@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) );
bool constraintTerm_isStringLiteral (constraintTerm c) /*@*/
{
llassert (c != NULL);
- if (c->kind == EXPRNODE)
+ if (c->kind == CTT_EXPR)
{
if (exprNode_knownStringValue(c->value.expr) )
{
{
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 ) )
{
temp = exprNode_getLongValue (term->value.expr);
term->value.intlit = (int)temp;
- term->kind = INTLITERAL;
+ term->kind = CTT_INTLITERAL;
}
}
return term;
/*@exposed@*/ sRef constraintTerm_getSRef (constraintTerm t)
{
llassert (constraintTerm_isDefined(t) );
- llassert (t->kind == SREF);
+ llassert (t->kind == CTT_SREF);
return (t->value.sref);
}
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;
}
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;
}
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:
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;
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:
}
-cstring constraintTerm_print (constraintTerm term) /*@*/
+cstring constraintTerm_unparse (constraintTerm term) /*@*/
{
cstring s;
s = cstring_undefined;
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;
{
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))
{
return FALSE;
}
}
- else if (term->kind == EXPRNODE)
+ else if (term->kind == CTT_EXPR)
{
return FALSE;
}
{
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))
{
BADBRANCH;
}
}
- else if (term->kind == EXPRNODE)
+ else if (term->kind == CTT_EXPR)
{
BADBRANCH;
}
{
llassert (t != NULL);
- llassert (t->kind == EXPRNODE);
+ llassert (t->kind == CTT_EXPR);
return t->value.expr;
/*@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;
}
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;
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;
}
break;
- case INTLITERAL:
+ case CTT_INTLITERAL:
fprintf (f, "%ld\n", t->value.intlit);
break;
switch (kind)
{
- case SREF:
+ case CTT_SREF:
{
sRef s;
char * term;
}
break;
- case EXPRNODE:
+ case CTT_EXPR:
{
sRef s;
char * term;
break;
- case INTLITERAL:
+ case CTT_INTLITERAL:
{
int i;
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:
{
switch (term->kind)
{
- case EXPRNODE:
+ case CTT_EXPR:
if (exprNode_isNumLiteral (term->value.expr) ||
exprNode_isStringLiteral (term->value.expr) ||
exprNode_isCharLiteral (term->value.expr) )
return FALSE;
}
- case INTLITERAL:
+ case CTT_INTLITERAL:
return TRUE;
- case SREF:
+ case CTT_SREF:
if ( sRef_isConst (term->value.sref) )
{
return TRUE;
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;
}
{ 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); ;
*/
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
** 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;
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;
/* 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
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;