From 3d5af57657a639ba6fcc4005d16e7313f875e519 Mon Sep 17 00:00:00 2001
From: drl7x <drl7x>
Date: Wed, 11 Dec 2002 23:12:30 +0000
Subject: [PATCH] Fixed fatal errors in constraint checking.

Added a special in cscanner.l so that maxSet and maxRead are handled correctly.
---
 src/cscanner.l | 62 ++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 53 insertions(+), 9 deletions(-)

diff --git a/src/cscanner.l b/src/cscanner.l
index 77d33d0..4bb02db 100644
--- a/src/cscanner.l
+++ b/src/cscanner.l
@@ -3226,25 +3226,43 @@ processSpec (int tok)
   
   if (s_inSpecPart)
     {
-      
-#if 0
 
+      /*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 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
-
-#endif
-
 	{
 	  setTokLengthT (length);
 	  RETURN_TOK (tok);
@@ -3268,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;
+    }
+}
-- 
2.45.2