From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 17 May 2013 21:04:34 +0000 (-0400)
Subject: Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive mode.
X-Git-Tag: cvc5-1.0.0~7287^2~33^2~15
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aef543d74c4fb23a86ad2986d67e7fc7f11d1feb;p=cvc5.git

Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive mode.

Thanks to David Cok for raising this issue.
---

diff --git a/src/parser/parser.h b/src/parser/parser.h
index d13fbf2d6..0761b4cda 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -462,6 +462,11 @@ public:
     d_input->parseError(msg);
   }
 
+  /** Unexpectedly encountered an EOF */
+  inline void unexpectedEOF(const std::string& msg) throw(ParserException) {
+    d_input->parseError(msg, true);
+  }
+
   /**
    * If we are parsing only, don't raise an exception; if we are not,
    * raise a parse error with the given message.  There is no actual
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 7bbcb85d8..29b6e0fbb 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1346,6 +1346,8 @@ symbol[std::string& id,
         PARSER_STATE->checkDeclaration(id, check, type);
       }
     }
+  | UNTERMINATED_QUOTED_SYMBOL EOF
+    { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); }
   ;
 
 /**
@@ -1539,6 +1541,9 @@ BVSGE_TOK : 'bvsge';
 QUOTED_SYMBOL
   : '|' ~('|' | '\\')* '|'
   ;
+UNTERMINATED_QUOTED_SYMBOL
+  : '|' ~('|' | '\\')*
+  ;
 
 /**
  * Matches a keyword from the input. A keyword is a simple symbol prefixed