From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Wed, 20 Oct 2010 20:41:10 +0000 (+0000)
Subject: Fixing minor whitespace bug in the parser
X-Git-Tag: cvc5-1.0.0~8797
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4af7ae6c56153347035656a2596254c1a8a17668;p=cvc5.git

Fixing minor whitespace bug in the parser
---

diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h
index fad5edc1e..a29462687 100644
--- a/src/parser/bounded_token_buffer.h
+++ b/src/parser/bounded_token_buffer.h
@@ -18,6 +18,11 @@
  ** an exception. Only use this factory if you *know* that the grammar
  ** has bounded lookahead (e.g., if you've set the k parameter in the 
  ** parser.
+ **
+ ** NOTE: ANTLR3 puts "hidden" tokens into this buffer too, so
+ ** pathological inputs can exceed the k token lookahead, even if
+ ** your grammar really is LL(k). Be sure that irrelevant tokens
+ ** are SKIP()'d and not "hidden".
  **/
 
 #ifndef	__CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 979f2a7c3..8fa1ca55a 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -555,10 +555,10 @@ fragment DIGIT : '0'..'9';
 /**
  * Matches and skips whitespace in the input and ignores it.
  */
-WHITESPACE : (' ' | '\t' | '\f' | '\r' | '\n') { $channel = HIDDEN;; };
+WHITESPACE : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP();; };
 
 /**
  * Matches the comments and ignores them
  */
-COMMENT : '%' (~('\n' | '\r'))* { $channel = HIDDEN;; };
+COMMENT : '%' (~('\n' | '\r'))* { SKIP();; };
 
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 8bbbbe0be..f125826d3 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -646,7 +646,7 @@ USER_VALUE
  * Matches and skips whitespace in the input.
  */
 WHITESPACE
-  :  (' ' | '\t' | '\f' | '\r' | '\n')+             { $channel = HIDDEN;; }
+  :  (' ' | '\t' | '\f' | '\r' | '\n')+             { SKIP();; }
   ;
 
 /**
@@ -672,7 +672,7 @@ STRING_LITERAL
  * Matches the comments and ignores them
  */
 COMMENT
-  : ';' (~('\n' | '\r'))*                    { $channel = HIDDEN;; }
+  : ';' (~('\n' | '\r'))*                    { SKIP();; }
   ;
 
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f549d2148..705eee4d4 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -661,7 +661,7 @@ fragment SIMPLE_SYMBOL
  * Matches and skips whitespace in the input.
  */
 WHITESPACE
-  : (' ' | '\t' | '\f' | '\r' | '\n')+ { $channel = HIDDEN; }
+  : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }
   ;
 
 /**
@@ -727,7 +727,7 @@ STRING_LITERAL
  * Matches the comments and ignores them
  */
 COMMENT
-  : ';' (~('\n' | '\r'))* { $channel = HIDDEN; }
+  : ';' (~('\n' | '\r'))* { SKIP(); }
   ;