diff options
| -rw-r--r-- | configure.ac | 5 | ||||
| -rw-r--r-- | src/expr/command.cpp | 13 | ||||
| -rw-r--r-- | src/expr/command.h | 11 | ||||
| -rw-r--r-- | src/main/driver.cpp | 20 |
4 files changed, 32 insertions, 17 deletions
diff --git a/configure.ac b/configure.ac index 0eebd62d1..1c14f8c6e 100644 --- a/configure.ac +++ b/configure.ac @@ -783,12 +783,15 @@ AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH]) if test -z "$CXXTESTGEN"; then AC_PATH_PROG(CXXTESTGEN, cxxtestgen.py, [], [$CXXTEST:$PATH]) fi +if test -z "$CXXTESTGEN"; then + AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST:$PATH]) +fi if test "$enable_unit_testing" = "no"; then AC_MSG_NOTICE([unit tests disabled by user request.]) CXXTESTGEN= CXXTEST= elif test -z "$CXXTESTGEN"; then - AC_MSG_NOTICE([unit tests disabled, neither cxxtestgen.pl nor cxxtestgen.py found.]) + AC_MSG_NOTICE([unit tests disabled, could not find cxxtestgen.pl or cxxtestgen.py or cxxtestgen]) elif test -z "$CXXTEST"; then CXXTEST=`dirname "$CXXTESTGEN"` AC_MSG_CHECKING([for location of CxxTest headers]) diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 648c64388..b058292f3 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -91,6 +91,10 @@ bool Command::ok() const throw() { return d_commandStatus == NULL || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL; } +bool Command::fail() const throw() { + return d_commandStatus != NULL && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL; +} + void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { invoke(smtEngine); printResult(out); @@ -1048,11 +1052,11 @@ std::string GetInfoCommand::getFlag() const throw() { void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() { try { - SExpr response = smtEngine->getInfo(d_flag); + vector<SExpr> v; + v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); + v.push_back(smtEngine->getInfo(d_flag)); stringstream ss; - ss << SExpr(SExpr::Keyword(d_flag)) - << ' ' - << response; + ss << SExpr(v); d_result = ss.str(); d_commandStatus = CommandSuccess::instance(); } catch(UnrecognizedOptionException&) { @@ -1136,7 +1140,6 @@ void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() { v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); v.push_back(smtEngine->getOption(d_flag)); stringstream ss; - ss << SExpr(v); d_result = ss.str(); d_commandStatus = CommandSuccess::instance(); diff --git a/src/expr/command.h b/src/expr/command.h index 4657755e7..0f517e7f2 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -211,9 +211,18 @@ public: std::string toString() const throw(); - /** Either the command hasn't run yet, or it completed successfully. */ + /** + * Either the command hasn't run yet, or it completed successfully + * (CommandSuccess, not CommandUnsupported or CommandFailure). + */ bool ok() const throw(); + /** + * The command completed in a failure state (CommandFailure, not + * CommandSuccess or CommandUnsupported). + */ + bool fail() const throw(); + /** Get the command status (it's NULL if we haven't run yet). */ const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; } diff --git a/src/main/driver.cpp b/src/main/driver.cpp index ca5dfad93..1e6f87d24 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -293,12 +293,12 @@ int runCvc4(int argc, char* argv[], Options& opts) { // have the replay parser use the file's declarations replayParser->useDeclarationsFrom(parser); } - while((cmd = parser->nextCommand()) && status) { + while(status && (cmd = parser->nextCommand())) { if(dynamic_cast<QuitCommand*>(cmd) != NULL) { delete cmd; break; } - status = doCommand(smt, cmd, opts) && status; + status = doCommand(smt, cmd, opts); delete cmd; } // Remove the parser @@ -352,16 +352,18 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& opts) { return true; } - // assume no error - bool status = true; - CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd); if(seq != NULL) { + // assume no error + bool status = true; + for(CommandSequence::iterator subcmd = seq->begin(); - subcmd != seq->end(); + status && subcmd != seq->end(); ++subcmd) { - status = doCommand(smt, *subcmd, opts) && status; + status = doCommand(smt, *subcmd, opts); } + + return status; } else { if(opts[options::verbosity] > 0) { *opts[options::out] << "Invoking: " << *cmd << endl; @@ -372,8 +374,6 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& opts) { } else { cmd->invoke(&smt); } - status = status && cmd->ok(); + return !cmd->fail(); } - - return status; } |