Fixing minor whitespace bug in the parser

diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h
index fad5edc1ee7f82e23a68cb4880d1a19c909d86ee..a29462687447d4f3dbe4371bd3e136e764f2cd59 100644 (file)
--- 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 979f2a7c30e44000efdfeb762e6fecce84dfa021..8fa1ca55a12b01440928852271f96da5edb3a9b7 100644 (file)
--- 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 8bbbbe0bea486e001cd12926a2557bb2d645d9c9..f125826d3b5034810fec7d8e0dcca9b4f435fecc 100644 (file)
--- 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 f549d21482d3c59521ca87ef56d6ce673d655f2f..705eee4d4a1fd65d8c14624925feb0620001f9ee 100644 (file)
--- 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(); }
   ;