X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/1ac6313d90a797f38280d75b2a63655579080ac6..8ac07c2e07220278ae0f39c18b03fe4344e97122:/src/sRef.c

diff --git a/src/sRef.c b/src/sRef.c
index 3402521..0e6dc60 100644
--- a/src/sRef.c
+++ b/src/sRef.c
@@ -2039,6 +2039,72 @@ sRef_closeEnough (sRef s1, sRef s2)
   BADEXIT;
 }
 
+/*
+  drl add 12/24/2000
+  s is an sRef of a formal paramenter in a function call constraint
+  we trys to return a constraint expression derived from the actual parementer of a function call.
+*/
+constraintExpr sRef_fixConstraintParam ( sRef s, exprNodeList args)
+{
+  constraintExpr ce;
+
+  if (sRef_isInvalid (s))
+    llfatalbug((message("Invalid sRef")));
+
+  switch (s->kind)
+    {
+    case SK_RESULT:
+      {
+	ce = constraintExpr_makeTermsRef (s);
+	return ce;
+      }
+    case SK_FIELD:
+      {
+	sRef temp;
+	
+	temp = (sRef_makeField (sRef_fixBaseParam (s->info->field->rec, args),
+			      s->info->field->field));
+	ce = constraintExpr_makeTermsRef (temp);
+	return ce;
+      }
+    case SK_PTR:
+      {
+	sRef temp;
+	temp = (sRef_makePointer (sRef_fixBaseParam (s->info->ref, args)));
+	ce = constraintExpr_makeTermsRef (temp);
+	return ce;
+      }
+
+    case SK_ARRAYFETCH:
+       {
+	sRef temp;
+	temp = sRef_fixBaseParam (s, args);
+	ce = constraintExpr_makeTermsRef (temp);
+	return ce;
+      }
+    case SK_CVAR:
+       ce = constraintExpr_makeTermsRef (s);
+       return ce;
+    case SK_PARAM:
+      llassert(exprNodeList_size (args) > s->info->paramno);
+	{
+	  exprNode e = exprNodeList_nth (args, s->info->paramno);
+
+	  llassert( !(exprNode_isError (e)) );
+	  ce = constraintExpr_makeExprNode (e);
+	  return ce;
+	}
+
+    default:
+      llcontbug ((message("Trying to do fixConstraintParam on nonparam, nonglobal: %s for function with arguments %s", sRef_unparse (s), exprNodeList_unparse(args) ) ));
+      ce = constraintExpr_makeTermsRef (s);
+      return ce;
+    }
+
+  
+
+}
+
 /*@exposed@*/ sRef
 sRef_fixBaseParam (/*@returned@*/ sRef s, exprNodeList args)
 {
@@ -3472,7 +3538,7 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
 	  res->definfo = alinfo_update (res->definfo, other->definfo);
 	  sRef_clearDerived (other);
 	  sRef_clearDerived (res);
-	  	}
+	}
       else if (res->defstate == SS_DEAD 
 	       && ((sRef_isOnly (other) && sRef_definitelyNull (other))
 		   || (other->defstate == SS_UNDEFINED
@@ -3487,7 +3553,7 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
 	    {
 	      res->defstate = SS_DEAD;
 	    }
-
+	  
 	  sRef_clearDerived (other);
 	  sRef_clearDerived (res);
 	}
@@ -4985,7 +5051,7 @@ void sRef_setNullState (sRef s, nstate n, fileloc loc)
     }
 }
 
-void sRef_setNullTerminatedStateInnerComplete (sRef s, struct _bbufinfo b, fileloc loc) {
+void sRef_setNullTerminatedStateInnerComplete (sRef s, struct _bbufinfo b, /*@unused@*/ fileloc loc) {
    
   switch (b.bufstate) {
      case BB_NULLTERMINATED:
@@ -5978,7 +6044,8 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
       
       if (ctype_isMutable (s->type) 
 	  && !ctype_isPointer (arr->type) 
-	  && !alkind_isStatic (arr->aliaskind))
+	  && !alkind_isStatic (arr->aliaskind)
+	  && !alkind_isStack (arr->aliaskind)) /* evs - 2000-06-20: don't pass stack allocation to members */
 	{
 	  s->aliaskind = arr->aliaskind;
 	}
@@ -6709,6 +6776,10 @@ bool sRef_hasName (sRef s)
     }
 }
 
+bool sRef_sameObject (sRef s1, sRef s2)
+{
+  return sRef_sameName(s1, s2);
+}
 bool
 sRef_sameName (sRef s1, sRef s2)
 {
@@ -8806,7 +8877,7 @@ cstring sRef_nullMessage (sRef s)
   BADEXIT;
 }
 
-cstring sRef_ntMessage (sRef s)
+/*@observer@*/ cstring sRef_ntMessage (sRef s)
 {
   llassert (sRef_isValid (s));
 
@@ -9034,7 +9105,8 @@ struct _bbufinfo sRef_getNullTerminatedState (sRef p_s) {
    struct _bbufinfo BUFSTATE_UNKNOWN;
    BUFSTATE_UNKNOWN.bufstate = BB_NOTNULLTERMINATED;
    BUFSTATE_UNKNOWN.size = 0;
-
+   BUFSTATE_UNKNOWN.len = 0;
+   
    if (sRef_isValid(p_s))
       return p_s->bufinfo;
    return BUFSTATE_UNKNOWN; 
@@ -9089,3 +9161,24 @@ void sRef_resetLen(sRef p_s) {
 		llfatalbug (message ("sRef_setLen passed an invalid sRef\n"));
 	}
 }
+
+/*drl7x 11/28/2000 */
+
+bool sRef_isFixedArray (sRef p_s) /*@*/ {
+  ctype c;
+  c = sRef_getType (p_s);
+  return ( ctype_isFixedArray (c) );
+}
+
+long int sRef_getArraySize (sRef p_s) /*@*/ {
+  ctype c;
+  llassert (sRef_isFixedArray(p_s) );
+  DPRINTF (( message ("sRef_getArraySize getting array size for %s", sRef_unparse(p_s) )  ));
+  
+  c = sRef_getType (p_s);
+
+  return (ctype_getArraySize (c) );
+}
+
+
+