From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 27 Sep 2017 07:43:30 +0000 (-0700)
Subject: Fix seeking for buffered input (#1145)
X-Git-Tag: cvc5-1.0.0~5607
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2567868bdf5664e95f998e76512c84d2c63f09a2;p=cvc5.git

Fix seeking for buffered input (#1145)

CVC4's implementation of seek was calculating the pointer difference
between the current position in the input and the seek point to
determine how many characters to consume. This was causing problems when
ANTLR was seeking to a pointer on a line after the current line because
it would result in a big number of characters to consume because each
line is allocated separately.  This resulted in issue #1113, where CVC4
was computing a large number of characters to consume and would block
until it received all of them.  This commit fixes and simplifies the
code by simply consuming characters until the seek point is reached
without computing a count beforehand.
---

diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp
index 8a4bcdebb..e9e861e17 100644
--- a/src/parser/antlr_line_buffered_input.cpp
+++ b/src/parser/antlr_line_buffered_input.cpp
@@ -294,10 +294,8 @@ static void bufferedInputSeek(pANTLR3_INT_STREAM is, ANTLR3_MARKER seekPoint) {
   assert(!line_buffered_input->line_buffer->isPtrBefore(
       (uint8_t*)seekPoint, input->line, input->charPositionInLine));
 
-  ssize_t count = (ssize_t)(seekPoint - (ANTLR3_MARKER)(input->nextChar));
-  while (count > 0) {
+  while ((ANTLR3_MARKER)(input->nextChar) != seekPoint) {
     is->consume(is);
-    count--;
   }
 }