Improved tracking of state change locations. Added +showdeephistory

[splint.git] / src / clabstract.c

diff --git a/src/clabstract.c b/src/clabstract.c
index db7300c787f9bd215e9e1405bf413dc27507a514..304d0edc97c209f6251a17f953928b755506cf24 100644 (file)
--- a/src/clabstract.c
+++ b/src/clabstract.c
@@ -31,10 +31,7 @@
 # include "splintMacros.nf"
 # include "llbasic.h"
 # include "cgrammar.h"
-
-# ifndef NOLCL
 # include "usymtab_interface.h"
-# endif
 
 # include "structNames.h"
 # include "nameChecks.h"
@@ -498,7 +495,12 @@ static /*@dependent@*/ uentryList currentParamList;
 /*drl added 3-28-2002*/
 /* this function takes a list of paramentar and generates a list
    of constraints.
-   Currently the only constraints gnerated are MaxSet(p) >= 0 for all pointers
+*/
+
+/* drl modified 10/23/2002
+
+The current semantics are generated constraints of the form MaxSet(p) >= 0 and MaxRead(p) >= 0 for all pointers
+unless the @out@ annotation has been applied to a parameter, then we only want to generate maxSet(p) > = 0
 */
 
 void  setImplictfcnConstraints (void)
@@ -527,13 +529,24 @@ void  setImplictfcnConstraints (void)
          DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
        }
       /*drl 4/26/01
-       chagned this is MaxSet(s) == 0 to MaxSet(s) >= 0 */
-      
+       chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0 */
       c = constraint_makeSRefWriteSafeInt (s, 0);
-      /* constraint_makeSRefSetBufferSize (s, 0); */
+      
       implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
+
+      /*drl 10/23/2002 added support for out*/
+      if (!uentry_isOut(el) )
+       {
+         c = constraint_makeSRefReadSafeInt (s, 0);
+      
+         implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
+       }
+       
+      
     }
   end_uentryList_elements;
+  DPRINTF((message("implicitFcnConstraints has been set to %s\n",
+                  constraintList_print(implicitFcnConstraints) ) ));
 }
 
 
@@ -1810,7 +1823,7 @@ handleEnum (cstring id)
     }
   else
     {
-      return (declareEnum (id, enumNameList_new ()));
+      return (ctype_createForwardEnum (id));
     }
 }
 
@@ -1850,12 +1863,14 @@ void setNewStyle ()              { flipNewStyle = TRUE; }
   uentryList_elements (params, current)
     {
       uentry_setParam (current);
-      uentry_setSref (current, sRef_makeParam (paramno, ctype_unknown, stateInfo_makeLoc (uentry_whereLast (current))));
+      uentry_setSref (current, sRef_makeParam 
+                     (paramno, ctype_unknown, 
+                      stateInfo_makeLoc (uentry_whereLast (current), SA_DECLARED)));
       paramno++;
     } end_uentryList_elements;
 
   setGenericParamList (params);
-  g_expectingTypeName = TRUE; 
+  cscannerHelp_setExpectingTypeName ();
 
   return params;
 }
@@ -1872,7 +1887,7 @@ void setNewStyle ()              { flipNewStyle = TRUE; }
       
       setGenericParamList (params);
       flipOldStyle = FALSE;
-      g_expectingTypeName = TRUE; 
+      cscannerHelp_setExpectingTypeName ();
     }
  
   return (params); 
@@ -1892,7 +1907,9 @@ doVaDcl ()
       if (i >= 0)
        {
          fileloc loc = context_getSaveLocation ();
-         e = uentry_makeVariableSrefParam (id, c, loc, sRef_makeParam (i, c, stateInfo_makeLoc (loc)));
+         e = uentry_makeVariableSrefParam 
+           (id, c, loc, 
+            sRef_makeParam (i, c, stateInfo_makeLoc (loc, SA_DECLARED)));
        }
       else
        {
@@ -2165,6 +2182,7 @@ sRef checkStateClausesId (uentry ue)
 
 sRef checkbufferConstraintClausesId (uentry ue)
 {
+  sRef sr;
   cstring s = uentry_rawName (ue);
 
   if (cstring_equalLit (s, "result"))
@@ -2179,8 +2197,14 @@ sRef checkbufferConstraintClausesId (uentry ue)
        }
     }
   
-  DPRINTF (("constrant id: %s", uentry_unparseFull (ue)));
-  return sRef_saveCopy (uentry_getSref (ue)); /*@i523 why the saveCopy? */
+  DPRINTF (("constraint id: %s", uentry_unparseFull (ue)));
+  sr = uentry_getSref (ue);
+
+  if (sRef_isInvalid (sr) )
+    {
+      llfatalerrorLoc (cstring_makeLiteral("Macro defined constants can not be used in function constraints unless they are specifed with the constant annotation.  To use a macro defined constant include an annotation of the form /*@constant <type> <name>=<value>@*/ somewhere before the function constraint.  This restriction may be removed in future releases if it is determined to be excessively burdensome." ));
+    }
+  return sRef_saveCopy (sr); /*@i523 why the saveCopy? */
 }
 
 void checkModifiesId (uentry ue)