Fix seeking for buffered input (#1145)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 27 Sep 2017 07:43:30 +0000 (00:43 -0700)
committerGitHub <noreply@github.com>
Wed, 27 Sep 2017 07:43:30 +0000 (00:43 -0700)
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.

src/parser/antlr_line_buffered_input.cpp

index 8a4bcdebbfbb76dfccc4bb721b2c014c4e7677bd..e9e861e17fd2167c776ec9193aecf64df2319bf5 100644 (file)
@@ -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--;
   }
 }