From 47139e8b11b0f11289a1b6cca46cd62e0814eaa3 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Tue, 29 Apr 2014 19:07:20 -0400 Subject: [PATCH] fix was compiler warning in antlr_input, crashing test case with the old fix --- src/parser/antlr_input.cpp | 8 ++++---- test/regress/regress0/Makefile.am | 2 ++ test/regress/regress0/errorcrash.smt2 | 9 +++++++++ 3 files changed, 15 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress0/errorcrash.smt2 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)) -- 2.30.2