X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/2f2892c2eae871c76b3acfd77a8accfb9f4c7322..53306cab3dabf761f459f8f5fdc4b30eca6ec707:/src/cscanner.l

diff --git a/src/cscanner.l b/src/cscanner.l
index 074bd55..4bb02db 100644
--- a/src/cscanner.l
+++ b/src/cscanner.l
@@ -3226,19 +3226,43 @@ processSpec (int tok)
   
   if (s_inSpecPart)
     {
+
+      /*drl 12/11/2002
+	patched to fix assert failures in constraint code.
+	Added the else if test so that splint does not treat MaxSet and MaxRead
+	as identifies*/
+	
       if (s_whichSpecPart == QMODIFIES
 	  || s_whichSpecPart == QDEFINES
 	  || s_whichSpecPart == QUSES 
 	  || s_whichSpecPart == QALLOCATES
 	  || s_whichSpecPart == QSETS
-	  || s_whichSpecPart == QRELEASES
-	  || s_whichSpecPart == QPRECLAUSE
-	  || s_whichSpecPart == QPOSTCLAUSE
-	  || s_whichSpecPart == QINVARIANT)
+	  || s_whichSpecPart == QRELEASES)
+	
 	{
+	  DPRINTF((message("Treating specifaction keyword %s as an identifiers.  (This corresponds to"
+			   " token %d and we're in the  specification denoted by %d see cgrammar_tokens.h"
+			   " for an explanation of these numbers",
+			   yytext, tok, s_whichSpecPart)
+		   ));
+			   
 	  ; /* Allow specificiation keywords to be used as identifiers in these contexts. */
 	}
-      else 
+      else if ( (s_whichSpecPart == QPRECLAUSE
+		 || s_whichSpecPart == QPOSTCLAUSE
+		 || s_whichSpecPart == QINVARIANT )
+		&&  (!isConstraintToken(tok) )
+	      )
+	{
+	  DPRINTF((message("Treating specifaction keyword %s as an identifiers.  (This corresponds to"
+			   " token %d and we're in the  specification denoted by %d see cgrammar_tokens.h"
+			   " for an explanation of these numbers",
+			   yytext, tok, s_whichSpecPart)
+		   ));
+	  
+	  /* Allow specificiation keywords to be used as identifiers in these contexts. */
+	}
+      else
 	{
 	  setTokLengthT (length);
 	  RETURN_TOK (tok);
@@ -3262,3 +3286,29 @@ void cscanner_clearExpectingMetaStateName ()
   llassert (expectingMetaStateName);
   expectingMetaStateName = FALSE;
 }
+
+/*drl added 12/11/2002
+  Tell whether a token has special meaning
+  within a function constraint
+*/
+
+/*uncomment the additional if statement tests
+  when minSet and minRead are supported
+*/
+int isConstraintToken(int tok)
+{
+  if (   tok == QMAXSET
+	 || tok == QMAXREAD
+      
+	 /*      || tok == QMINREAD
+		 || tok == QMINSET */
+
+     )
+    {
+      return TRUE;
+    }
+  else
+    {
+      return FALSE;
+    }
+}