From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 29 Apr 2014 23:07:20 +0000 (-0400)
Subject: fix was compiler warning in antlr_input, crashing test case with the old fix
X-Git-Tag: cvc5-1.0.0~6948
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=47139e8b11b0f11289a1b6cca46cd62e0814eaa3;p=cvc5.git

fix was compiler warning in antlr_input, crashing test case with the old fix
---

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 88b43eb0e..ee4e2ff37 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -374,9 +374,9 @@ std::string parseErrorHelper(const char* lineStart, int charPositionInLine, cons
         string word = slice.substr(caretPos, (caretPosOrig - caretPos + 1));
         int messagePosSt = message.find(word);
         int messagePosEn = messagePosSt + (caretPosOrig - caretPos);
-        if( messagePosSt < string::npos &&
+        if( (size_t)messagePosSt < string::npos &&
             (messagePosSt == 0 || !isSimpleChar(message[messagePosSt-1]) ) &&
-            (messagePosEn+1 == message.size() || !isSimpleChar(message[messagePosEn+1]) ) ) {
+            ((size_t)messagePosEn+1 == message.size() || !isSimpleChar(message[messagePosEn+1]) ) ) {
           // ^the complicated if statement is just 'whole-word' match
           Debug("friendlyparser") << "[friendlyparser] Feeling good." << std::endl;
         }
@@ -398,9 +398,9 @@ std::string parseErrorHelper(const char* lineStart, int charPositionInLine, cons
         Debug("friendlyparser") << "[friendlyparser] nearest word = " << word << std::endl;
         int messagePosSt = message.find(word);
         int messagePosEn = messagePosSt + (nearestWordEn - nearestWordSt + 1);
-        if( messagePosSt < string::npos &&
+        if( (size_t)messagePosSt < string::npos &&
             (messagePosSt == 0 || !isSimpleChar(message[messagePosSt-1]) ) &&
-            (messagePosEn+1 == message.size() || !isSimpleChar(message[messagePosEn+1]) ) ) {
+            ((size_t)messagePosEn+1 == message.size() || !isSimpleChar(message[messagePosEn+1]) ) ) {
           // ^the complicated if statement is just 'whole-word' match
           Debug("friendlyparser") << "[friendlyparser] strong evidence that caret should be at "
                                   << nearestWordSt << std::endl;
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index f16e18bdf..521993db3 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -170,6 +170,7 @@ if CVC4_BUILD_PROFILE_COMPETITION
 else
 TESTS += \
 	error.cvc \
+	errorcrash.smt2 \
 	arrayinuf_error.smt2
 endif
 
@@ -177,6 +178,7 @@ endif
 EXTRA_DIST += \
 	subranges.cvc \
 	arrayinuf_error.smt2 \
+	errorcrash.smt2 \
 	error.cvc
 
 # synonyms for "check" in this directory
diff --git a/test/regress/regress0/errorcrash.smt2 b/test/regress/regress0/errorcrash.smt2
new file mode 100644
index 000000000..59d5b2014
--- /dev/null
+++ b/test/regress/regress0/errorcrash.smt2
@@ -0,0 +1,9 @@
+; EXIT: 1
+; EXPECT-ERROR: (error "Parse Error: errorcrash.smt2:5.29: Symbol 'Array' not declared as a type")
+(set-logic QF_UF)
+(declare-sort U 0)
+(declare-fun x () (Array U U))
+(declare-fun y () (Array U U))
+(assert (= x y))
+(check-sat)
+(get-value (x y))