X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/3cf0f8a8618810aaaf7ece472e8b2c28a9c7b4f0..ef2aa32aebac950c1784a2dd25f0fa299b8840da:/src/uentry.c

diff --git a/src/uentry.c b/src/uentry.c
index 823b9ea..5da16f3 100644
--- a/src/uentry.c
+++ b/src/uentry.c
@@ -572,15 +572,76 @@ constraintList uentry_getFcnPreconditions (uentry 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))
 	    {
-	      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;
+	    }
 	}
 	
     }
@@ -590,7 +651,6 @@ constraintList uentry_getFcnPreconditions (uentry ue)
 }
 
 
-
 static /*@only@*/ fileloc setLocation (void)
 {
   fileloc fl = context_getSaveLocation ();
@@ -895,6 +955,15 @@ uentry_makeFunctionAux (cstring n, ctype t,
   
   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;
 
@@ -1283,6 +1352,44 @@ uentry_setPreconditions (uentry ue, /*@owned@*/ constraintList preconditions)
     }
 }
 
+/*
+  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
 */
@@ -2895,6 +3002,11 @@ void uentry_makeVarFunction (uentry ue)
   /*drl*/
   ue->info->fcn->preconditions = constraintList_undefined;
   /*end */
+
+  /*drl 12/28/2000*/
+  ue->info->fcn->postconditions = constraintList_undefined;
+  /*end */
+
   
   if (ctype_isFunction (ue->utype))
     {
@@ -3933,6 +4045,14 @@ static uentry
 
   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);
 }
 
@@ -5907,6 +6027,15 @@ ufinfo_copy (ufinfo u)
   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;
 }
 
@@ -9604,7 +9733,7 @@ void uentry_checkName (uentry ue)
 
 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);