u->exitCode = XK_NEVERESCAPE;
u->kind = US_NORMAL;
- return (u);
+ /*@i23@*/ return (u);
}
void
if (context_getFlag (FLG_NOLIB))
{
ctype boolt = ctype_bool;
+ /* evs 2000-07-24: bool is now treated as abstract (always) */
+
+ uentry boolentry = uentry_makeBoolDatatype (YES);
+ usymtab_supGlobalEntry (boolentry);
+ context_addBoolAccess ();
- if (context_getFlag (FLG_ABSTRACTBOOL))
- {
- uentry boolentry = uentry_makeBoolDatatype (YES);
-
- usymtab_supGlobalEntry (boolentry);
- context_addBoolAccess ();
- }
- else
- {
- uentry boolentry = uentry_makeBoolDatatype (NO);
-
- usymtab_supGlobalEntry (boolentry);
- }
-
/*
** We supply values 0 and 1 for the constants, so things like
** while (TRUE) can be interpreted correctly.
bool staticEntry = FALSE;
int eindex;
- DPRINTF (("Sup entry aux: %s", uentry_unparseFull (e)));
-
/* static tags in global scope */
if (st->lexlevel == fileScope
&& (!(uentry_isStatic (e)) || uentry_isAnyTag (e)))
/*@modifies globtab@*/
{
usymId uid;
-
+
if (uentry_isAbstractDatatype (e))
{
- uid = usymtab_supAbstractTypeEntry (e, FALSE);
+ uid = usymtab_supAbstractTypeEntry (e, FALSE);
}
else
{
- uid = usymtab_supEntryAux (globtab, e, FALSE);
+ uid = usymtab_supEntryAux (globtab, e, FALSE);
}
-
+
if (sRef_modInFunction ())
{
recordFunctionType (globtab->entries[uid]);
/*@modifies globtab, e@*/
{
usymId uid;
-
uid = usymtab_supEntryAux (globtab, e, FALSE);
if (dodef)
{
uentry ue = usymtab_getTypeEntry (uid);
-
uentry_setDatatype (ue, uid);
}
usymId uid = usymtab_getIndex (globtab, k);
if (uid == NOT_FOUND) return USYMIDINVALID;
- if (!(uentry_isDatatype (usymtab_getTypeEntry (uid)))) return USYMIDINVALID;
+
+ if (!(uentry_isDatatype (usymtab_getTypeEntry (uid)))) {
+ return USYMIDINVALID;
+ }
return uid;
}
{
check (fputc ('\n', fout) == (int) '\n');
}
+
+ lastekind = KINVALID;
+
+ fprintf(fout, ";; Library constraints\n");
+ for (i = 0; i < utab->nentries; i++)
+ {
+ uentry thisentry = utab->entries[i];
+
+ if (uentry_isFunction (thisentry) )
+ {
+ constraintList preconditions;
+ constraintList postconditions;
+
+ preconditions = uentry_getFcnPreconditions (thisentry);
+ postconditions = uentry_getFcnPostconditions (thisentry);
+
+ if ( constraintList_isDefined(preconditions) ||
+ constraintList_isDefined(postconditions) )
+ {
+ fprintf(fout,"%s\n", uentry_rawName(thisentry) );
+ if (constraintList_isDefined(preconditions) )
+ {
+ fprintf(fout,"pre:\n");
+ constraintList_dump(preconditions, fout);
+ fprintf (fout, ";; end precondition constraints\n" );
+ constraintList_free(preconditions);
+ }
+ else
+ {
+ fprintf(fout,"pre:EMPTY\n");
+ }
+ if (constraintList_isDefined(postconditions) )
+ {
+ fprintf(fout,"post:\n");
+ constraintList_dump(postconditions, fout);
+ fprintf (fout, ";; end precondition constraints\n" );
+ constraintList_free(postconditions);
+ }
+ else
+ {
+ fprintf(fout,"post:EMPTY\n");
+ }
+ }
+
+ }
+ }
+
+
+
}
void usymtab_load (FILE *f)
s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
}
+ /*DRL added 6/21/01
+ to handle reading of buffer overflow related constraints
+ */
+ while (fgets (s, MAX_DUMP_LINE_LENGTH, f) != NULL
+ && *s == ';')
+ {
+ ; /* ignore ;-comments */
+ }
+
+ while (s != NULL && *s != ';')
+ {
+ constraintList preconditions;
+ constraintList postconditions;
+
+ cstring name = getWord(&s);
+ cstring temp;
+ ue = usymtab_lookup ( name );
+
+ cstring_free(name);
+
+ preconditions = constraintList_undefined;
+ postconditions = constraintList_undefined;
+
+ if (!uentry_isValid(ue) )
+ {
+ llfatalbug ((message("Invalid uentry for %s library file may be corrupted", s) ));
+ }
+ s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
+
+ temp = getWord(&s);
+
+ if (cstring_compare (temp,"pre:") == 0 )
+ {
+ preconditions = constraintList_undump(f);
+ }
+ cstring_free(temp);
+
+ s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
+
+ temp = getWord(&s);
+ if (cstring_compare (temp,"post:") == 0 )
+ {
+ postconditions = constraintList_undump(f);
+ }
+
+ cstring_free(temp);
+
+ uentry_setPreconditions (ue, preconditions);
+ uentry_setPostconditions (ue, postconditions);
+
+ s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
+ }
+
dbgload = FALSE;
sfree (os);
}
specialClauses_elements (clauses, cl)
{
- sRefTest tst = specialClause_getPostTestFunction (cl);
- sRefSet rfs = specialClause_getRefs (cl);
-
-
- sRefSet_elements (rfs, el)
- {
- sRef base = sRef_getRootBase (el);
-
- if (sRef_isResult (base))
- {
- ;
- }
- else if (sRef_isParam (base))
+ if (specialClause_isAfter (cl))
+ { /* evs - 2000 07 10 - added this */
+ sRefTest tst = specialClause_getPostTestFunction (cl);
+ sRefSet rfs = specialClause_getRefs (cl);
+
+ sRefSet_elements (rfs, el)
{
- sRef sr = sRef_updateSref (base);
-
- sr = sRef_fixBase (el, sr);
-
+ sRef base = sRef_getRootBase (el);
- if (tst != NULL && !tst (sr))
+ if (sRef_isResult (base))
{
- if (optgenerror
- (specialClause_postErrorCode (cl),
- message ("%s storage %qcorresponds to "
- "storage listed in %q clause",
- specialClause_postErrorString (cl, sr),
- sRef_unparseOpt (sr),
- specialClause_unparseKind (cl)),
- g_currentloc))
+ ;
+ }
+ else if (sRef_isParam (base))
+ {
+ sRef sr = sRef_updateSref (base);
+ sr = sRef_fixBase (el, sr);
+
+ if (tst != NULL && !tst (sr))
{
- sRefShower ss = specialClause_getPostTestShower (cl);
-
- if (ss != NULL)
+ if (optgenerror
+ (specialClause_postErrorCode (cl),
+ message ("%s storage %qcorresponds to "
+ "storage listed in %q clause",
+ specialClause_postErrorString (cl, sr),
+ sRef_unparseOpt (sr),
+ specialClause_unparseKind (cl)),
+ g_currentloc))
{
- ss (sr);
- }
+ sRefShower ss = specialClause_getPostTestShower (cl);
+
+ if (ss != NULL)
+ {
+ ss (sr);
+ }
+ }
}
-
- }
- }
- else
- {
- if (sRef_isMeaningful (el))
+ }
+ else
{
- BADBRANCH;
+ if (sRef_isMeaningful (el))
+ {
+ BADBRANCH;
+ }
}
- }
- } end_sRefSet_elements ;
-
+ } end_sRefSet_elements ;
+ }
} end_specialClauses_elements ;
}
-
-
+
/*
** check parameters on return
*/
}
}
- llassertprint (utab->kind != US_TBRANCH && utab->kind != US_FBRANCH
- && utab->kind != US_CBRANCH && utab->kind != US_SWITCH,
- ("exitScope: in branch: %s", usymtab_unparseStack()));
+ if (utab->kind == US_TBRANCH || utab->kind == US_FBRANCH
+ || utab->kind == US_CBRANCH || utab->kind == US_SWITCH) {
+
+ if (context_inMacro ()) {
+ /* evs 2000-07-25 */
+ /* Unparseable macro may end inside nested scope. Deal with it. */
+
+ llerror (FLG_SYNTAX, message ("Problem parsing macro body of %s (unbalanced scopes). Attempting to recover, recommend /*@notfunction@*/ before macro definition.",
+ context_inFunctionName ()));
+
+ while (utab->kind == US_TBRANCH
+ || utab->kind == US_FBRANCH
+ || utab->kind == US_CBRANCH
+ || utab->kind == US_SWITCH)
+ {
+ utab = utab->env;
+ llassert (utab != GLOBAL_ENV);
+ }
+ } else {
+ llcontbug (message ("exitScope: in branch: %s", usymtab_unparseStack ()));
+ /*@-branchstate@*/
+ } /*@=branchstate@*/
+ }
/*
** check all variables in scope were used
int i;
aliasTable_free (u->aliases);
-
+ // environmentTable_free (u->environment);
refTable_free (u->reftable, u->nentries);
if (u == filetab || u == globtab)
BADEXIT;
}
+// oid usymtab_testInRange (sRef s, int index) /*@globals utab;@*/
+// {
+// /*@i22*/
+// /*@-globs*/
+// environmentTable_testInRange (utab->environment, s, index);
+// /*@=globs*/
+// }
+// void usymtab_postopVar (sRef sr) /*@globals utab;@*/
+// {
+// environmentTable_postOpvar (utab->environment, sr);
+
+// }
+// /* doesn't do much check here assumes checking is done before call*/
+// void usymtab_addExactValue(sRef s1, int val)
+// {
+// /*@i22@*/ utab->environment = environmentTable_addExactValue (utab->environment, s1, val);
+// }
+
void usymtab_addMustAlias (sRef s, sRef al)
/*@modifies utab@*/
{
andersk / splint.git / blobdiff