# include "structNames.h"
# include "nameChecks.h"
+/*@i223*/
+/*@-type*/
static /*@dependent@*/ uentry posRedeclared = uentry_undefined;
static /*@only@*/ fileloc posLoc = fileloc_undefined;
static int nuentries = 0;
}
printf ("\n");
- printf ("Total Annotations: %d (%d decls, %d sharable, %d indirect)\n", alltotals, totdecls, totshdecls, totidecls); }
+ printf ("Total Annotations: %d (%d decls, %d sharable, %d indirect)\n", alltotals, totdecls, totshdecls, totidecls);
+}
extern void uentry_tallyAnnots (uentry u, ancontext kind)
{
}
}
+
+/*drl7x*/
+constraintList uentry_getFcnPreconditions (uentry ue)
+{
+ if (uentry_isValid (ue))
+ {
+ {
+ if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
+ {
+ uentry_makeVarFunction (ue);
+ }
+
+ //llassert (uentry_isFunction (ue));
+ //llassert ((ue->info->fcn->preconditions));
+ //llassert ((ue->info->fcn->preconditions));
+ if (!uentry_isFunction (ue))
+ {
+ TPRINTF ( (message ("called uentry_getFcnPreconditions on nonfunction %s",
+ uentry_unparse (ue) ) ) );
+ if (!uentry_isSpecified (ue) )
+ {
+ TPRINTF((message ("called uentry_getFcnPreconditions on nonfunction %s",
+ uentry_unparse (ue) ) ));
+ return constraintList_undefined;
+ }
+
+
+ return constraintList_undefined;
+ }
+
+ if (ue->info->fcn->preconditions)
+ {
+ return constraintList_copy (ue->info->fcn->preconditions);
+ }
+ else
+ {
+ return NULL;
+ }
+ }
+
+ }
+
+ return constraintList_undefined;
+
+}
+
+
+/*drl
+ 12/28/2000
+*/
+constraintList uentry_getFcnPostconditions (uentry ue)
+{
+ if (uentry_isValid (ue))
+ {
+ {
+ if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
+ {
+ uentry_makeVarFunction (ue);
+ }
+
+ //llassert (uentry_isFunction (ue));
+ //llassert ((ue->info->fcn->preconditions));
+ /* if (!uentry_isSpecified (ue) )
+ {
+ TPRINTF((message ("called uentry_getFcnPostconditions on nonfunction %s",
+ uentry_unparse (ue) ) ));
+ // return constraintList_undefined;
+ }*/
+
+ if (!uentry_isFunction (ue))
+ {
+ /*llcontbug*/ TPRINTF( (message ("called uentry_getFcnPostconditions on nonfunction %s",
+ uentry_unparse (ue) ) ) );
+ return constraintList_undefined;
+ }
+
+ if (ue->info->fcn->postconditions)
+ {
+ return constraintList_copy (ue->info->fcn->postconditions);
+ }
+ else
+ {
+ return NULL;
+ }
+ }
+
+ }
+
+ return constraintList_undefined;
+
+}
+
+
static /*@only@*/ fileloc setLocation (void)
{
fileloc fl = context_getSaveLocation ();
e->info->fcn->mods = sRefSet_undefined;
e->info->fcn->specclauses = NULL;
+
+ /*drl 11 29 2000*/
+ e->info->fcn->preconditions = NULL;
+ /*end drl*/
+
+ /*drl 12 28 2000*/
+ e->info->fcn->postconditions = NULL;
+ /*end drl*/
+
checkGlobalsModifies (e, mods);
e->info->fcn->mods = mods;
void uentry_setSpecialClauses (uentry ue, specialClauses clauses)
{
llassert (uentry_isFunction (ue));
- llassert (ue->info->fcn->specclauses == NULL);
+ llassert (!specialClauses_isDefined (ue->info->fcn->specclauses));
ue->info->fcn->specclauses = clauses;
specialClauses_checkAll (ue);
}
}
+void
+uentry_setPreconditions (uentry ue, /*@owned@*/ constraintList preconditions)
+{
+ if (sRef_modInFunction ())
+ {
+ llparseerror
+ (message ("Precondition list not in function context. "
+ "A precondition list can only appear following the parameter list "
+ "in a function declaration or header."));
+
+ /*@-mustfree@*/ return; /*@=mustfree@*/
+ }
+
+ if (uentry_isValid (ue))
+ {
+ {
+ if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
+ {
+ uentry_makeVarFunction (ue);
+ }
+
+ llassertfatal (uentry_isFunction (ue));
+ // llassert (sRefSet_isUndefined (ue->info->fcn->mods));
+
+ ue->info->fcn->preconditions = preconditions;
+ }
+
+ }
+ else
+ {
+ //
+ }
+}
+
+/*
+ drl
+ added 12/28/2000
+*/
+void
+uentry_setPostconditions (uentry ue, /*@owned@*/ constraintList postconditions)
+{
+ if (sRef_modInFunction ())
+ {
+ llparseerror
+ (message ("Postcondition list not in function context. "
+ "A postcondition list can only appear following the parameter list "
+ "in a function declaration or header."));
+
+ /*@-mustfree@*/ return; /*@=mustfree@*/
+ }
+
+ if (uentry_isValid (ue))
+ {
+ {
+ if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
+ {
+ uentry_makeVarFunction (ue);
+ }
+
+ llassertfatal (uentry_isFunction (ue));
+ // llassert (sRefSet_isUndefined (ue->info->fcn->mods));
+
+ ue->info->fcn->postconditions = postconditions;
+ }
+
+ }
+ else
+ {
+ //
+ }
+}
+
/*
** requires: new and old are functions
*/
}
/* put other BufState Qualifiers here */
- } else {
+ } else {
+ cstring s = uentry_getName(ue);
llfatalbug(message("INTERNAL Error: we have a NULL BufState \
- struct for identifier %s\n", uentry_getName(ue) ) );
+ struct for identifier %s\n", s) );
}
} else if (ctype_isFunction (ct)) { /* We have to handle function */
while (ctype_isFixedArray (base)) {
base = ctype_baseArrayPtr (base);
}
-
+
if (ctype_isIncompleteArray (base)) {
base = ctype_baseArrayPtr (base);
if (ctype_isArray (base)) {
- (void) optgenerror (FLG_INCOMPLETETYPE,
- message ("Function parameter %q is incomplete type (inner array must have bounds): %s",
- uentry_getName (ue),
- ctype_unparse (ct)),
- uentry_whereLast (ue));
+ if (!uentry_hasName (ue)) {
+ (void) optgenerror (FLG_INCOMPLETETYPE,
+ message ("Unnamed function parameter %d is incomplete type (inner array must have bounds): %s",
+ i + 1,
+ ctype_unparse (ct)),
+ uentry_whereLast (ue));
+ } else {
+ (void) optgenerror (FLG_INCOMPLETETYPE,
+ message ("Function parameter %q is incomplete type (inner array must have bounds): %s",
+ uentry_getName (ue),
+ ctype_unparse (ct)),
+ uentry_whereLast (ue));
+ }
}
}
is a pointer or array and allocate a `bbufinfo' struct accordingly */
if( ctype_isArray (t) || ctype_isPointer(t)) {
- e->info->var->bufinfo = dmalloc( sizeof(*e->info->var->bufinfo) );
+ /*@i222@*/e->info->var->bufinfo = dmalloc( sizeof(*e->info->var->bufinfo) );
e->info->var->bufinfo->bufstate = BB_NOTNULLTERMINATED;
s->bufinfo.bufstate = BB_NOTNULLTERMINATED;
} else {
ue->info->fcn->specclauses = NULL;
ue->info->fcn->defparams = uentryList_undefined;
+ /*drl*/
+ ue->info->fcn->preconditions = constraintList_undefined;
+ /*end */
+
+ /*drl 12/28/2000*/
+ ue->info->fcn->postconditions = constraintList_undefined;
+ /*end */
+
+
if (ctype_isFunction (ue->utype))
{
ue->sref = sRef_makeType (ctype_returnValue (ue->utype));
{
uentry e = uentry_alloc ();
+ DPRINTF (("Make datatype: %s / %s",
+ n, ctype_unparse (t)));
+
/* e->shallowCopy = FALSE; */
e->ukind = KDATATYPE;
e->uname = cstring_copy (n);
sRef_setAliasKind (e->sref, aliased, loc);
sRef_storeState (e->sref);
+
+ /*DRL ADDED 9-1-2000 */
+ e->info->var->bufinfo = NULL;
+
return (e);
}
bool uentry_hasSpecialClauses (uentry ue)
{
- return (uentry_isFunction (ue) && (ue->info->fcn->specclauses != NULL));
+ return (uentry_isFunction (ue) && specialClauses_isDefined (ue->info->fcn->specclauses));
}
specialClauses uentry_getSpecialClauses (uentry ue)
sRef_storeState (e->sref);
+ /*drl 111 30 2000*/
+ e->info->fcn->preconditions = NULL;
+ /* end drl */
+
+ /*drl 12 28 2000*/
+ e->info->fcn->postconditions = NULL;
+ /* end drl */
+
return (e);
}
{
llassert (uentry_isValid (v));
+ DPRINTF (("Dumping entry: %s", uentry_unparseFull (v)));
+
switch (v->ukind)
{
case KINVALID:
exkind exk = sRef_getExKind (v->sref);
chkind chk = v->info->var->checked;
+ DPRINTF (("Dumping var"));
+
if (dss == SS_UNKNOWN
&& nst == NS_UNKNOWN
&& alk == AK_IMPTEMP
return ctype_unknown;
}
+ /*
+ ** Sadly, a kludge...
+ */
+
+ if (ctype_isUserBool (e->info->datatype->type)) {
+ return ctype_bool;
+ }
+
return e->info->datatype->type;
}
ctype uentry_getRealType (uentry e)
{
- ctype ct;
+ ctype ct;
typeId uid = USYMIDINVALID;
if (uentry_isInvalid (e))
if (uentry_isAbstractType (e))
{
ct = uentry_getAbstractType (e);
+
+ if (ctype_isManifestBool (ct)) {
+ return ct;
+ }
+
llassert (ctype_isUA (ct));
uid = ctype_typeId (ct);
ct = uentry_getType (e);
- if (ctype_isUserBool (ct)) return ct;
+ /* if (ctype_isUserBool (ct)) return ct; */
+
+ if (ctype_isManifestBool (ct)) {
+ return ctype_bool;
+ }
if (ctype_isUA (ct))
{
}
else
{
- return uentry_getRealType (usymtab_getTypeEntry (iid));
+ /* evs 2000-07-25: possible infinite recursion ? */
+ uentry ue2 = usymtab_getTypeEntry (iid);
+ llassertprint (ue2 != e, ("Bad recursion: %s", uentry_unparseFull (e)));
+
+ return uentry_getRealType (ue2);
}
}
else
}
ct = uentry_getType (e);
-
- if (ctype_isUserBool (ct)) return ct;
+
+ /* evs 2000-07-25 */
+ /* if (ctype_isUserBool (ct)) return ct; */
+
+ if (ctype_isManifestBool (ct)) {
+ return ctype_bool;
+ }
if (ctype_isUA (ct))
{
ret->nullstate = u->nullstate;
ret->defstate = u->defstate;
ret->checked = u->checked;
-
- return ret;
+ //make sure line ok
+ //ret->bufinfo = u->bufinfo;
+ /*@i334@*/ return ret;
}
static /*@only@*/ udinfo
ret->defparams = u->defparams;
ret->specclauses = specialClauses_copy (u->specclauses);
+ /*drl 11 30 2000 */
+ ret->preconditions = u->preconditions? constraintList_copy(u->preconditions): NULL;
+ /* end drl */
+
+
+ /*drl 11 30 2000 */
+ ret->postconditions = u->postconditions? constraintList_copy(u->postconditions): NULL;
+ /* end drl */
+
return ret;
}
checkGlobalsConformance (old, unew, mustConform, completeConform);
checkModifiesConformance (old, unew, mustConform, completeConform);
- if (unew->info->fcn->specclauses != NULL)
+ if (specialClauses_isDefined (unew->info->fcn->specclauses))
{
- if (old->info->fcn->specclauses == NULL)
+ if (!specialClauses_isDefined (old->info->fcn->specclauses))
{
if (optgenerror
(FLG_INCONDEFS,
}
else
{
+ DPRINTF (("YABA!"));
if (optgenerror
(FLG_INCONDEFS,
message ("%s %q %rdeclared with inconsistent type: %t",
{
if (ctype_isDefined (unew->info->datatype->type))
{
+ /*
+ ** bool is hard coded here, since it is built into LCL.
+ ** For now, we're stuck with LCL's types.
+ */
+
if (ctype_isDirectBool (old->utype) &&
cstring_equalLit (unew->uname, "bool"))
{
- if (!context_getFlag (FLG_ABSTRACTBOOL))
- {
+ /* if (!context_getFlag (FLG_ABSTRACTBOOL))
+ evs 2000-07-25: removed
+ */
unew->utype = ctype_bool;
- }
}
if (ctype_isUnknown (old->info->datatype->type))
}
else
{
+ DPRINTF (("Old: %s / New: %s",
+ uentry_unparseFull (old),
+ uentry_unparseFull (unew)));
+ DPRINTF (("Types: %s / %s",
+ ctype_unparse (old->info->datatype->type),
+ ctype_unparse (unew->info->datatype->type)));
+
if (ctype_matchDef (old->info->datatype->type,
- unew->info->datatype->type))
+ unew->info->datatype->type))
{
;
}
if (uentry_isDatatype (old) && uentry_isDatatype (unew))
{
+ DPRINTF (("Check datatype: %s / %s",
+ uentry_unparseFull (old),
+ uentry_unparseFull (unew)));
+
uentry_checkDatatypeConformance (old, unew, mustConform, completeConform);
}
return ue;
}
+/* new start modifications */
+
+void uentry_testInRange (uentry p_e, uentry cconstant) {
+ if( uentry_isValid(p_e) ) {
+ if( sRef_isValid (p_e->sref) ) {
+ char * t = cstring_toCharsSafe (uentry_unparse(cconstant) );
+ int index = atoi( t );
+ free (t);
+ usymtab_testInRange (p_e->sref, index);
+ }//end if
+ }//endif
+}
+
+void uentry_setStringLength (uentry p_e, uentry cconstant) {
+if( uentry_isValid(p_e) ) {
+ if( p_e->info != NULL) {
+ if( p_e->info->var != NULL) {
+ char *t = cstring_toCharsSafe (uentry_unparse(cconstant));
+ int length = atoi( t );
+ free (t);
+ p_e->info->var->bufinfo->len = length;
+ p_e->sref->bufinfo.len = length;
+ printf("Set string length of buff to %d \n", p_e->sref->bufinfo.size);
+ }//end if
+ }//endif
+}//end if
+}
+
+
+void uentry_setBufferSize (uentry p_e, exprNode cconstant) {
+if( uentry_isValid(p_e) ) {
+ if( p_e->info != NULL) {
+ if( p_e->info->var != NULL) {
+ int size = atoi(cstring_toCharsSafe(exprNode_unparse(cconstant) ) );
+ p_e->info->var->bufinfo->size = size;
+ p_e->sref->bufinfo.size = size;
+ printf("Set buffer size to %d \n", p_e->sref->bufinfo.size);
+ // fprintf(stderr, "For %s and %s\n", uentry_unparse(p_e) );
+ // fprintf(stderr, "and %d\n", size );
+
+ }//end if
+ }//endif
+}//end if
+}
+
/* start modifications */
/*
requires: p_e is defined, is a ptr/array variable
fprintf(stderr, "uentry:Error in setLen\n");
}
-
+/*@=type*/
andersk / splint.git / blobdiff