Merge

7 files changed, 207 insertions, 139 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 76eaf661..274ed534 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1803,13 +1803,37 @@ namespace Microsoft.Boogie {
     {

       selectors = new List<DatatypeSelector>();

     }

+

+    public override void Resolve(ResolutionContext rc) {

+      HashSet<string> selectorNames = new HashSet<string>();

+      foreach (DatatypeSelector selector in selectors) {

+        if (selector.Name.StartsWith("#")) {

+          rc.Error(selector.tok, "The selector must be a non-empty string");

+        }

+        else {

+          if (selectorNames.Contains(selector.Name))

+            rc.Error(this.tok, "The selectors for a constructor must be distinct strings");

+          else

+            selectorNames.Add(selector.Name);

+        }

+      }

+      base.Resolve(rc);

+    }

+    

+    public override void Typecheck(TypecheckingContext tc) {

+      CtorType outputType = this.OutParams[0].TypedIdent.Type as CtorType;

+      if (outputType == null || !outputType.IsDatatype()) {

+        tc.Error(tok, "The output type of a constructor must be a datatype");

+      }

+      base.Typecheck(tc);

+    }

   }

 

   public class DatatypeSelector : Function {

     public Function constructor;

     public int index;

     public DatatypeSelector(Function constructor, int index)

-      : base(constructor.tok, 

+      : base(constructor.InParams[index].tok, 

              constructor.InParams[index].Name + "#" + constructor.Name,

              new VariableSeq(new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.OutParams[0].TypedIdent.Type), true)),

              new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.InParams[index].TypedIdent.Type), false)) 

@@ -1817,6 +1841,7 @@ namespace Microsoft.Boogie {
       this.constructor = constructor;

       this.index = index;

     }

+

     public override void Emit(TokenTextWriter stream, int level) { }

   }

 

@@ -1830,8 +1855,8 @@ namespace Microsoft.Boogie {
     {

       this.constructor = constructor;

     }

-    public override void Emit(TokenTextWriter stream, int level) {

-    }

+

+    public override void Emit(TokenTextWriter stream, int level) { }

   }

 

   public class Function : DeclWithFormals {

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index e96c3fd1..62ebc77f 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -749,6 +749,7 @@ namespace Microsoft.Boogie {
         } else {

           stream.Write(level + 1, "invariant ");

         }

+        Cmd.EmitAttributes(stream, inv.Attributes);

         inv.Expr.Emit(stream);

         stream.WriteLine(";");

       }

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 84703a7c..a22ece7d 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -2820,6 +2820,10 @@ Contract.Requires(that != null);
       this.Arguments = arguments;

     }

 

+    public bool IsDatatype() {

+      return QKeyValue.FindBoolAttribute(Decl.Attributes, "datatype");

+    }

+

     //-----------  Cloning  ----------------------------------

     // We implement our own clone-method, because bound type variables

     // have to be created in the right way. It is /not/ ok to just clone

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 33172e7f..aed741d8 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -35,26 +35,30 @@ static StructuredCmd/*!*/ dummyStructuredCmd = new BreakCmd(Token.NoToken, null)
 ///the parsed program.

 ///</summary>

 public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

-Contract.Requires(filename != null);

-Contract.Requires(cce.NonNullElements(defines,true));

+  Contract.Requires(filename != null);

+  Contract.Requires(cce.NonNullElements(defines,true));

 

+  if (defines == null) {

+    defines = new List<string/*!*/>();

+  }

 

-  FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);

-  var ret = Parse(stream, filename, defines, out program);

-  stream.Close();

-  return ret;

+  if (filename == "stdin.bpl") {

+    var s = ParserHelper.Fill(Console.In, defines);

+    return Parse(s, filename, out program);

+  } else {

+    FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);

+    var s = ParserHelper.Fill(stream, defines);

+    var ret = Parse(s, filename, out program);

+    stream.Close();

+    return ret;

+  }

 }

 

 

-public static int Parse (Stream stream, string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

-Contract.Requires(stream != null);

-Contract.Requires(filename != null);

-Contract.Requires(cce.NonNullElements(defines,true));

+public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

+  Contract.Requires(s != null);

+  Contract.Requires(filename != null);

 

-  if (defines == null) {

-    defines = new List<string/*!*/>();

-  }

-  string s = ParserHelper.Fill(stream, defines);

   byte[]/*!*/ buffer = cce.NonNull(UTF8Encoding.Default.GetBytes(s));

   MemoryStream ms = new MemoryStream(buffer,false);

   Errors errors = new Errors();

@@ -66,6 +70,7 @@ Contract.Requires(cce.NonNullElements(defines,true));
     if (parser.errors.count == 0)

     {

       program = Pgm;

+      program.ProcessDatatypeConstructors();

       return 0;

     }

     else

@@ -111,10 +116,13 @@ CHARACTERS
   cr        = '\r'.

   lf        = '\n'.

   tab       = '\t'.

-

+  

   space = ' '.

   quote = '"'.

 

+  newLine = cr + lf.

+  regularStringChar = ANY - quote - newLine.

+

   nondigit = letter + special.

   nonquote = letter + digit + space + glyph.

 

@@ -124,7 +132,9 @@ TOKENS
   ident =  [ '\\' ] nondigit {nondigit | digit}.

   bvlit = digit {digit} 'b' 'v' digit {digit}.

   digits = digit {digit}.

-  string = quote {nonquote} quote.

+

+  string = quote { regularStringChar | "\\\"" } quote.

+

   float = digit {digit} '.' {digit}.

 

 COMMENTS FROM "/*" TO "*/" NESTED

@@ -776,6 +786,7 @@ WhileCmd<out WhileCmd/*!*/ wcmd>
      Expr guard;  Expr/*!*/ e;  bool isFree;

      List<PredicateCmd/*!*/> invariants = new List<PredicateCmd/*!*/>();

      StmtList/*!*/ body;

+     QKeyValue kv = null;

   .)

   "while"             (. x = t; .)

   Guard<out guard>    (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)

@@ -783,10 +794,11 @@ WhileCmd<out WhileCmd/*!*/ wcmd>
     [ "free"          (. isFree = true;  .)

     ]

     "invariant"

+    { Attribute<ref kv> }

     Expression<out e> (. if (isFree) {

-                           invariants.Add(new AssumeCmd(z, e));

+                           invariants.Add(new AssumeCmd(z, e, kv));

                          } else {

-                           invariants.Add(new AssertCmd(z, e));

+                           invariants.Add(new AssertCmd(z, e, kv));

                          }

                       .)

     ";"

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 9413cf30..1a2d7fda 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -389,6 +389,7 @@ namespace Microsoft.Boogie {
     public int /*(0:3)*/ ErrorTrace = 1;

     public bool IntraproceduralInfer = true;

     public bool ContractInfer = false;

+    public bool PrintAssignment = false;

     public int InlineDepth = -1;

     public bool UseUncheckedContracts = false;

     public bool SimplifyLogFileAppend = false;

@@ -447,6 +448,7 @@ namespace Microsoft.Boogie {
     public int EnhancedErrorMessages = 0;

     public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present

     public bool UseArrayTheory = false;

+    public bool UseLabels = true;

     public bool MonomorphicArrays {

       get {

         return UseArrayTheory || TypeEncodingMethod == TypeEncoding.Monomorphic;

@@ -561,6 +563,7 @@ namespace Microsoft.Boogie {
     public int StratifiedInlining = 0;

     public int StratifiedInliningOption = 0;

     public bool StratifiedInliningWithoutModels = false; // disable model generation for SI

+    public int StratifiedInliningVerbose = 0; // verbosity level

     public bool UseUnsatCoreForInlining = false;

     public int RecursionBound = 500;

     public string inferLeastForUnsat = null;

@@ -828,10 +831,6 @@ namespace Microsoft.Boogie {
           ps.GetNumericArgument(ref EnhancedErrorMessages, 2);

           return true;

 

-        case "contractInfer":

-          ContractInfer = true;

-          return true;

-

         case "inlineDepth":

           ps.GetNumericArgument(ref InlineDepth);

           return true;

@@ -1005,7 +1004,11 @@ namespace Microsoft.Boogie {
             }

           }

           return true;

-

+        case "siVerbose":

+          if (ps.ConfirmArgumentCount(1)) {

+            StratifiedInliningVerbose = Int32.Parse(cce.NonNull(args[ps.i]));

+          }

+          return true;

         case "recursionBound":

           if (ps.ConfirmArgumentCount(1)) {

             RecursionBound = Int32.Parse(cce.NonNull(args[ps.i]));

@@ -1222,7 +1225,10 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||

               ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||

               ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||

-              ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis)

+              ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||

+              ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||

+              ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||

+              ps.CheckBooleanFlag("printAssignment", ref PrintAssignment)

               ) {

             // one of the boolean flags matched

             return true;

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index fe77bcc1..5a6f8098 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -54,26 +54,30 @@ static StructuredCmd/*!*/ dummyStructuredCmd = new BreakCmd(Token.NoToken, null)
 ///the parsed program.

 ///</summary>

 public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

-Contract.Requires(filename != null);

-Contract.Requires(cce.NonNullElements(defines,true));

+  Contract.Requires(filename != null);

+  Contract.Requires(cce.NonNullElements(defines,true));

 

+  if (defines == null) {

+    defines = new List<string/*!*/>();

+  }

 

-  FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);

-  var ret = Parse(stream, filename, defines, out program);

-  stream.Close();

-  return ret;

+  if (filename == "stdin.bpl") {

+    var s = ParserHelper.Fill(Console.In, defines);

+    return Parse(s, filename, out program);

+  } else {

+    FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);

+    var s = ParserHelper.Fill(stream, defines);

+    var ret = Parse(s, filename, out program);

+    stream.Close();

+    return ret;

+  }

 }

 

 

-public static int Parse (Stream stream, string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

-Contract.Requires(stream != null);

-Contract.Requires(filename != null);

-Contract.Requires(cce.NonNullElements(defines,true));

+public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

+  Contract.Requires(s != null);

+  Contract.Requires(filename != null);

 

-  if (defines == null) {

-    defines = new List<string/*!*/>();

-  }

-  string s = ParserHelper.Fill(stream, defines);

   byte[]/*!*/ buffer = cce.NonNull(UTF8Encoding.Default.GetBytes(s));

   MemoryStream ms = new MemoryStream(buffer,false);

   Errors errors = new Errors();

@@ -1089,6 +1093,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		Expr guard;  Expr/*!*/ e;  bool isFree;

 		List<PredicateCmd/*!*/> invariants = new List<PredicateCmd/*!*/>();

 		StmtList/*!*/ body;

+		QKeyValue kv = null;

 		

 		Expect(40);

 		x = t; 

@@ -1101,11 +1106,14 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 				isFree = true;  

 			}

 			Expect(41);

+			while (la.kind == 25) {

+				Attribute(ref kv);

+			}

 			Expression(out e);

 			if (isFree) {

-			 invariants.Add(new AssumeCmd(z, e));

+			 invariants.Add(new AssumeCmd(z, e, kv));

 			} else {

-			 invariants.Add(new AssertCmd(z, e));

+			 invariants.Add(new AssertCmd(z, e, kv));

 			}

 			

 			Expect(7);

diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index e3d131e0..cfef86c7 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -259,39 +259,39 @@ public class Scanner {
 		for (int i = 48; i <= 57; ++i) start[i] = 9;

 		for (int i = 34; i <= 34; ++i) start[i] = 6;

 		start[92] = 1; 

-		start[59] = 10; 

-		start[40] = 11; 

-		start[41] = 12; 

-		start[58] = 47; 

-		start[44] = 13; 

-		start[91] = 14; 

-		start[93] = 15; 

-		start[60] = 48; 

-		start[62] = 49; 

-		start[123] = 16; 

-		start[125] = 50; 

-		start[61] = 51; 

-		start[42] = 17; 

-		start[8660] = 20; 

-		start[8658] = 22; 

-		start[8656] = 23; 

-		start[38] = 24; 

-		start[8743] = 26; 

-		start[124] = 52; 

-		start[8744] = 28; 

-		start[33] = 53; 

-		start[8800] = 32; 

-		start[8804] = 33; 

-		start[8805] = 34; 

-		start[43] = 54; 

-		start[45] = 36; 

-		start[47] = 37; 

-		start[37] = 38; 

-		start[172] = 39; 

-		start[8704] = 42; 

-		start[8707] = 43; 

-		start[955] = 44; 

-		start[8226] = 46; 

+		start[59] = 12; 

+		start[40] = 13; 

+		start[41] = 14; 

+		start[58] = 49; 

+		start[44] = 15; 

+		start[91] = 16; 

+		start[93] = 17; 

+		start[60] = 50; 

+		start[62] = 51; 

+		start[123] = 18; 

+		start[125] = 52; 

+		start[61] = 53; 

+		start[42] = 19; 

+		start[8660] = 22; 

+		start[8658] = 24; 

+		start[8656] = 25; 

+		start[38] = 26; 

+		start[8743] = 28; 

+		start[124] = 54; 

+		start[8744] = 30; 

+		start[33] = 55; 

+		start[8800] = 34; 

+		start[8804] = 35; 

+		start[8805] = 36; 

+		start[43] = 56; 

+		start[45] = 38; 

+		start[47] = 39; 

+		start[37] = 40; 

+		start[172] = 41; 

+		start[8704] = 44; 

+		start[8707] = 45; 

+		start[955] = 46; 

+		start[8226] = 48; 

 		start[Buffer.EOF] = -1;

 

 	}

@@ -576,7 +576,8 @@ public class Scanner {
 				else {t.kind = 2; break;}

 			case 6:

 				if (ch == '"') {AddCh(); goto case 7;}

-				else if (ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~') {AddCh(); goto case 6;}

+				else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}

+				else if (ch == 92) {AddCh(); goto case 10;}

 				else {goto case 0;}

 			case 7:

 				{t.kind = 4; break;}

@@ -591,125 +592,136 @@ public class Scanner {
 				else if (ch == '.') {AddCh(); goto case 8;}

 				else {t.kind = 3; break;}

 			case 10:

-				{t.kind = 7; break;}

+				if (ch == '"') {AddCh(); goto case 11;}

+				else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}

+				else if (ch == 92) {AddCh(); goto case 10;}

+				else {goto case 0;}

 			case 11:

-				{t.kind = 8; break;}

+				recEnd = pos; recKind = 4;

+				if (ch == '"') {AddCh(); goto case 7;}

+				else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}

+				else if (ch == 92) {AddCh(); goto case 10;}

+				else {t.kind = 4; break;}

 			case 12:

-				{t.kind = 9; break;}

+				{t.kind = 7; break;}

 			case 13:

-				{t.kind = 11; break;}

+				{t.kind = 8; break;}

 			case 14:

-				{t.kind = 15; break;}

+				{t.kind = 9; break;}

 			case 15:

-				{t.kind = 16; break;}

+				{t.kind = 11; break;}

 			case 16:

-				{t.kind = 25; break;}

+				{t.kind = 15; break;}

 			case 17:

-				{t.kind = 42; break;}

+				{t.kind = 16; break;}

 			case 18:

-				{t.kind = 47; break;}

+				{t.kind = 25; break;}

 			case 19:

-				{t.kind = 50; break;}

+				{t.kind = 42; break;}

 			case 20:

-				{t.kind = 51; break;}

+				{t.kind = 47; break;}

 			case 21:

-				{t.kind = 52; break;}

+				{t.kind = 50; break;}

 			case 22:

-				{t.kind = 53; break;}

+				{t.kind = 51; break;}

 			case 23:

-				{t.kind = 55; break;}

+				{t.kind = 52; break;}

 			case 24:

-				if (ch == '&') {AddCh(); goto case 25;}

-				else {goto case 0;}

+				{t.kind = 53; break;}

 			case 25:

-				{t.kind = 56; break;}

+				{t.kind = 55; break;}

 			case 26:

-				{t.kind = 57; break;}

+				if (ch == '&') {AddCh(); goto case 27;}

+				else {goto case 0;}

 			case 27:

-				{t.kind = 58; break;}

+				{t.kind = 56; break;}

 			case 28:

-				{t.kind = 59; break;}

+				{t.kind = 57; break;}

 			case 29:

-				{t.kind = 62; break;}

+				{t.kind = 58; break;}

 			case 30:

-				{t.kind = 63; break;}

+				{t.kind = 59; break;}

 			case 31:

-				{t.kind = 64; break;}

+				{t.kind = 62; break;}

 			case 32:

-				{t.kind = 65; break;}

+				{t.kind = 63; break;}

 			case 33:

-				{t.kind = 66; break;}

+				{t.kind = 64; break;}

 			case 34:

-				{t.kind = 67; break;}

+				{t.kind = 65; break;}

 			case 35:

-				{t.kind = 68; break;}

+				{t.kind = 66; break;}

 			case 36:

-				{t.kind = 70; break;}

+				{t.kind = 67; break;}

 			case 37:

-				{t.kind = 71; break;}

+				{t.kind = 68; break;}

 			case 38:

-				{t.kind = 72; break;}

+				{t.kind = 70; break;}

 			case 39:

-				{t.kind = 74; break;}

+				{t.kind = 71; break;}

 			case 40:

-				{t.kind = 78; break;}

+				{t.kind = 72; break;}

 			case 41:

-				{t.kind = 79; break;}

+				{t.kind = 74; break;}

 			case 42:

-				{t.kind = 81; break;}

+				{t.kind = 78; break;}

 			case 43:

-				{t.kind = 83; break;}

+				{t.kind = 79; break;}

 			case 44:

-				{t.kind = 85; break;}

+				{t.kind = 81; break;}

 			case 45:

-				{t.kind = 86; break;}

+				{t.kind = 83; break;}

 			case 46:

-				{t.kind = 87; break;}

+				{t.kind = 85; break;}

 			case 47:

+				{t.kind = 86; break;}

+			case 48:

+				{t.kind = 87; break;}

+			case 49:

 				recEnd = pos; recKind = 10;

-				if (ch == '=') {AddCh(); goto case 18;}

-				else if (ch == ':') {AddCh(); goto case 45;}

+				if (ch == '=') {AddCh(); goto case 20;}

+				else if (ch == ':') {AddCh(); goto case 47;}

 				else {t.kind = 10; break;}

-			case 48:

+			case 50:

 				recEnd = pos; recKind = 17;

-				if (ch == '=') {AddCh(); goto case 55;}

-				else if (ch == ':') {AddCh(); goto case 31;}

+				if (ch == '=') {AddCh(); goto case 57;}

+				else if (ch == ':') {AddCh(); goto case 33;}

 				else {t.kind = 17; break;}

-			case 49:

+			case 51:

 				recEnd = pos; recKind = 18;

-				if (ch == '=') {AddCh(); goto case 29;}

+				if (ch == '=') {AddCh(); goto case 31;}

 				else {t.kind = 18; break;}

-			case 50:

+			case 52:

 				recEnd = pos; recKind = 26;

-				if (ch == '|') {AddCh(); goto case 41;}

+				if (ch == '|') {AddCh(); goto case 43;}

 				else {t.kind = 26; break;}

-			case 51:

+			case 53:

 				recEnd = pos; recKind = 29;

-				if (ch == '=') {AddCh(); goto case 56;}

+				if (ch == '=') {AddCh(); goto case 58;}

 				else {t.kind = 29; break;}

-			case 52:

-				if (ch == '|') {AddCh(); goto case 27;}

-				else if (ch == '{') {AddCh(); goto case 40;}

+			case 54:

+				if (ch == '|') {AddCh(); goto case 29;}

+				else if (ch == '{') {AddCh(); goto case 42;}

 				else {goto case 0;}

-			case 53:

+			case 55:

 				recEnd = pos; recKind = 73;

-				if (ch == '=') {AddCh(); goto case 30;}

+				if (ch == '=') {AddCh(); goto case 32;}

 				else {t.kind = 73; break;}

-			case 54:

+			case 56:

 				recEnd = pos; recKind = 69;

-				if (ch == '+') {AddCh(); goto case 35;}

+				if (ch == '+') {AddCh(); goto case 37;}

 				else {t.kind = 69; break;}

-			case 55:

+			case 57:

 				recEnd = pos; recKind = 61;

-				if (ch == '=') {AddCh(); goto case 57;}

+				if (ch == '=') {AddCh(); goto case 59;}

 				else {t.kind = 61; break;}

-			case 56:

+			case 58:

 				recEnd = pos; recKind = 60;

-				if (ch == '>') {AddCh(); goto case 21;}

+				if (ch == '>') {AddCh(); goto case 23;}

 				else {t.kind = 60; break;}

-			case 57:

+			case 59:

 				recEnd = pos; recKind = 54;

-				if (ch == '>') {AddCh(); goto case 19;}

+				if (ch == '>') {AddCh(); goto case 21;}

 				else {t.kind = 54; break;}

 

 		}