X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/11ed4f45e321c24d9340dc277c54e1d2c9cd0046..7bec2f0111c222467685f17220484fce4fa77800:/src/uentry.c

diff --git a/src/uentry.c b/src/uentry.c
index d12a8a4..5da16f3 100644
--- a/src/uentry.c
+++ b/src/uentry.c
@@ -30,6 +30,8 @@
 # include "structNames.h"
 # include "nameChecks.h"
 
+/*@i223*/
+/*@-type*/
 static /*@dependent@*/ uentry posRedeclared = uentry_undefined;
 static /*@only@*/ fileloc posLoc = fileloc_undefined;
 static int nuentries = 0;
@@ -286,7 +288,8 @@ void printAnnots ()
     }
   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)
 {
@@ -555,6 +558,99 @@ static /*@observer@*/ cstring uentry_reDefDecl (uentry old, uentry unew)  /*@*/
     }
 }
 
+
+/*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 ();
@@ -859,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;
 
@@ -1141,7 +1246,7 @@ uentry_fixupSref (uentry ue)
 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);
@@ -1213,6 +1318,78 @@ uentry_setModifies (uentry ue, /*@owned@*/ sRefSet sr)
     }
 }
 
+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
 */
@@ -2080,9 +2257,10 @@ uentry_reflectQualifiers (uentry ue, qualList q)
 
                 } 
                 /* 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 */
 
@@ -2499,16 +2677,24 @@ uentry_isSpecialFunction (uentry ue)
   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));
+      }
     }
   }
 
@@ -2741,7 +2927,7 @@ static /*@only@*/ /*@notnull@*/
    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 {
@@ -2813,6 +2999,15 @@ void uentry_makeVarFunction (uentry ue)
   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)); 
@@ -3052,6 +3247,9 @@ uentry_makeUnspecFunction (cstring n, ctype t,
 {
   uentry e = uentry_alloc ();
 
+  DPRINTF (("Make datatype: %s / %s",
+	    n, ctype_unparse (t)));
+
   /* e->shallowCopy = FALSE; */
   e->ukind = KDATATYPE;
   e->uname = cstring_copy (n);
@@ -3637,6 +3835,10 @@ static /*@only@*/ uentry
   sRef_setAliasKind (e->sref, aliased, loc);
 
   sRef_storeState (e->sref);
+
+  /*DRL ADDED 9-1-2000 */
+  e->info->var->bufinfo = NULL;
+  
   return (e);
 }
 
@@ -3744,7 +3946,7 @@ bool uentry_hasGlobs (uentry ue)
 
 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)
@@ -3843,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);
 }
 
@@ -4281,6 +4491,8 @@ uentry_dumpAux (uentry v, bool isParam)
 {
   llassert (uentry_isValid (v));
 
+  DPRINTF (("Dumping entry: %s", uentry_unparseFull (v)));
+
   switch (v->ukind)
     {
     case KINVALID: 
@@ -4298,6 +4510,8 @@ uentry_dumpAux (uentry v, bool isParam)
 	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
@@ -5521,12 +5735,20 @@ uentry_getAbstractType (uentry e)
       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))
@@ -5544,6 +5766,11 @@ ctype uentry_getRealType (uentry e)
   if (uentry_isAbstractType (e))
     {
       ct = uentry_getAbstractType (e);      
+
+      if (ctype_isManifestBool (ct)) {
+	return ct;
+      }
+
       llassert (ctype_isUA (ct));
       
       uid = ctype_typeId (ct);
@@ -5556,7 +5783,11 @@ ctype uentry_getRealType (uentry e)
 
   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))
     {
@@ -5570,7 +5801,11 @@ ctype uentry_getRealType (uentry e)
 	}
       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
@@ -5606,8 +5841,13 @@ ctype uentry_getForceRealType (uentry e)
     }
   
   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))
     {
@@ -5754,8 +5994,9 @@ uvinfo_copy (uvinfo u)
   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
@@ -5786,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;
 }
 
@@ -7484,9 +7734,9 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old,
   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,
@@ -7642,6 +7892,7 @@ bool checkTypeConformance (/*@notnull@*/ uentry old, /*@notnull@*/ uentry unew,
 		}
 	      else
 		{
+		  DPRINTF (("YABA!"));
 		  if (optgenerror 
 		      (FLG_INCONDEFS,
 		       message ("%s %q %rdeclared with inconsistent type: %t",
@@ -7673,13 +7924,18 @@ uentry_checkDatatypeConformance (/*@notnull@*/ uentry old,
 {
   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))
@@ -7688,8 +7944,15 @@ uentry_checkDatatypeConformance (/*@notnull@*/ uentry old,
 	}
       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))
 	    {
 	      ;
 	    }
@@ -8060,6 +8323,10 @@ uentry_checkConformance (/*@unique@*/ /*@notnull@*/ uentry old,
 
   if (uentry_isDatatype (old) && uentry_isDatatype (unew))
     {
+      DPRINTF (("Check datatype: %s / %s",
+		uentry_unparseFull (old),
+		uentry_unparseFull (unew)));
+
       uentry_checkDatatypeConformance (old, unew, mustConform, completeConform);
     }
 
@@ -9464,11 +9731,24 @@ void uentry_checkName (uentry 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) {
-      int length = atoi(exprNode_unparse(cconstant) ); 
+      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);
@@ -9482,7 +9762,7 @@ 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(exprNode_unparse(cconstant) ); 
+      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);
@@ -9599,4 +9879,4 @@ void uentry_setLen (uentry p_e, int len)  {
   fprintf(stderr, "uentry:Error in setLen\n");
 }
 
-
+/*@=type*/