//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))
{
- BPRINTF ( (message ("called uentry_getFcnPreconditions on nonfunction %s",
+ /*llcontbug*/ TPRINTF( (message ("called uentry_getFcnPostconditions on nonfunction %s",
uentry_unparse (ue) ) ) );
return constraintList_undefined;
}
-
- return ue->info->fcn->preconditions;
+
+ if (ue->info->fcn->postconditions)
+ {
+ return constraintList_copy (ue->info->fcn->postconditions);
+ }
+ else
+ {
+ return NULL;
+ }
}
}
}
-
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;
}
}
+/*
+ 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
*/
/*drl*/
ue->info->fcn->preconditions = constraintList_undefined;
/*end */
+
+ /*drl 12/28/2000*/
+ ue->info->fcn->postconditions = constraintList_undefined;
+ /*end */
+
if (ctype_isFunction (ue->utype))
{
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);
}
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;
}
void uentry_testInRange (uentry p_e, uentry cconstant) {
if( uentry_isValid(p_e) ) {
- if( p_e->sref != NULL) {
+ if( sRef_isValid (p_e->sref) ) {
char * t = cstring_toCharsSafe (uentry_unparse(cconstant) );
int index = atoi( t );
free (t);