Fix a few segfaults in driver.

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/RELEASE-NOTES b/RELEASE-NOTES
index 243fa921597f7dc18fe01a7f02414a4e1420cb01..a68801d32f07d32a126aacd6c62244b45112c63c 100644 (file)
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -5,8 +5,8 @@ Release Notes for CVC4 1.0, October 2012
 If you run CVC4 without arguments, you will find yourself in an interactive
 CVC4 session, which expects commands in CVC4's native language (the so-called
 "presentation" language).  To use SMT-LIB, use the "--lang smt" option on the
-command line.  For stricter adherence to the standard, use "--smtlib2"
-(see below).
+command line.  For stricter adherence to the standard, use "--smtlib"
+(see below regarding SMT-LIB compliance).
 
 When a filename is given on the command line, the file's extension determines
 the language parser that's used (e.g., file.smt is SMT-LIB 1.2, file.smt2
@@ -69,7 +69,7 @@ Every effort has been made to make CVC4 compliant with the SMT-LIB 2.0
 standard (http://smtlib.org/).  However, when parsing SMT-LIB input,
 certain default settings don't match what is stated in the official
 standard.  To make CVC4 adhere more strictly to the standard, use the
-"--smtlib2" command-line option.  Even with this setting, CVC4 is
+"--smtlib" command-line option.  Even with this setting, CVC4 is
 somewhat lenient; some non-conforming input may still be parsed and
 processed.
 

diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index a5bd78abe53bad717b8e6fc0f168b47f4c081676..38a20b1cb1272f670552d190830ef4e244b4bc0e 100644 (file)
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -40,6 +40,8 @@ protected:
 public:
   CommandExecutor(ExprManager &exprMgr, Options &options);
 
+  virtual ~CommandExecutor() {}
+
   /**
    * Executes a command. Recursively handles if cmd is a command
    * sequence.  Eventually uses doCommandSingleton (which can be

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 3eba7ff6afd26aec9578ab5e1dcb364675b211d8..8f8e19f81ec3b83292ef0a1a67b43436878c6e41 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -63,7 +63,7 @@ namespace CVC4 {
     const char *progName;
 
     /** A pointer to the CommandExecutor (the signal handlers need it) */
-    CVC4::main::CommandExecutor* pExecutor;
+    CVC4::main::CommandExecutor* pExecutor = NULL;
 
   }/* CVC4::main namespace */
 }/* CVC4 namespace */
@@ -185,24 +185,21 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 
   // Create the expression manager using appropriate options
 # ifndef PORTFOLIO_BUILD
-  ExprManager exprMgr(opts);
+  ExprManager* exprMgr = new ExprManager(opts);
 # else
   vector<Options> threadOpts = parseThreadSpecificOptions(opts);
-  ExprManager exprMgr(threadOpts[0]);
+  ExprManager* exprMgr = new ExprManager(threadOpts[0]);
 # endif
 
 # ifndef PORTFOLIO_BUILD
-  CommandExecutor cmdExecutor(exprMgr, opts);
+  pExecutor = new CommandExecutor(*exprMgr, opts);
 # else
-  CommandExecutorPortfolio cmdExecutor(exprMgr, opts, threadOpts);
+  pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts);
 # endif
 
-  // give access to the signal handlers for stats output
-  pExecutor = &cmdExecutor;
-
   Parser* replayParser = NULL;
   if( opts[options::replayFilename] != "" ) {
-    ParserBuilder replayParserBuilder(&exprMgr, opts[options::replayFilename], opts);
+    ParserBuilder replayParserBuilder(exprMgr, opts[options::replayFilename], opts);
 
     if( opts[options::replayFilename] == "-") {
       if( inputFromStdin ) {
@@ -217,114 +214,122 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     *opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1);
   }
 
-  // Timer statistic
-  RegisterStatistic statTotalTime(&cmdExecutor.getStatisticsRegistry(), &s_totalTime);
-
-  // Filename statistics
-  ReferenceStat< const char* > s_statFilename("filename", filename);
-  RegisterStatistic statFilenameReg(&cmdExecutor.getStatisticsRegistry(), &s_statFilename);
-
-  // Parse and execute commands until we are done
-  Command* cmd;
-  bool status = true;
-  if( opts[options::interactive] ) {
-    InteractiveShell shell(exprMgr, opts);
-    Message() << Configuration::getPackageName()
-              << " " << Configuration::getVersionString();
-    if(Configuration::isSubversionBuild()) {
-      Message() << " [" << Configuration::getSubversionId() << "]";
-    }
-    Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
-              << " assertions:"
-              << (Configuration::isAssertionBuild() ? "on" : "off")
-              << endl;
-    if(replayParser != NULL) {
-      // have the replay parser use the declarations input interactively
-      replayParser->useDeclarationsFrom(shell.getParser());
-    }
-    while((cmd = shell.readCommand())) {
-      status = cmdExecutor.doCommand(cmd) && status;
-      delete cmd;
-    }
-  } else {
-    ParserBuilder parserBuilder(&exprMgr, filename, opts);
+  int returnValue = 0;
+  {
+    // Timer statistic
+    RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(), &s_totalTime);
+
+    // Filename statistics
+    ReferenceStat< const char* > s_statFilename("filename", filename);
+    RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(), &s_statFilename);
+
+    // Parse and execute commands until we are done
+    Command* cmd;
+    bool status = true;
+    if( opts[options::interactive] ) {
+      InteractiveShell shell(*exprMgr, opts);
+      Message() << Configuration::getPackageName()
+                << " " << Configuration::getVersionString();
+      if(Configuration::isSubversionBuild()) {
+        Message() << " [" << Configuration::getSubversionId() << "]";
+      }
+      Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
+                << " assertions:"
+                << (Configuration::isAssertionBuild() ? "on" : "off")
+                << endl;
+      if(replayParser != NULL) {
+        // have the replay parser use the declarations input interactively
+        replayParser->useDeclarationsFrom(shell.getParser());
+      }
+      while((cmd = shell.readCommand())) {
+        status = pExecutor->doCommand(cmd) && status;
+        delete cmd;
+      }
+    } else {
+      ParserBuilder parserBuilder(exprMgr, filename, opts);
 
-    if( inputFromStdin ) {
+      if( inputFromStdin ) {
 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
-      parserBuilder.withStreamInput(cin);
+        parserBuilder.withStreamInput(cin);
 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
-      parserBuilder.withLineBufferedStreamInput(cin);
+        parserBuilder.withLineBufferedStreamInput(cin);
 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
-    }
+      }
 
-    Parser *parser = parserBuilder.build();
-    if(replayParser != NULL) {
-      // have the replay parser use the file's declarations
-      replayParser->useDeclarationsFrom(parser);
-    }
-    while(status && (cmd = parser->nextCommand())) {
-      if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
+      Parser *parser = parserBuilder.build();
+      if(replayParser != NULL) {
+        // have the replay parser use the file's declarations
+        replayParser->useDeclarationsFrom(parser);
+      }
+      while(status && (cmd = parser->nextCommand())) {
+        if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
+          delete cmd;
+          break;
+        }
+        status = pExecutor->doCommand(cmd);
         delete cmd;
-        break;
       }
-      status = cmdExecutor.doCommand(cmd);
-      delete cmd;
+      // Remove the parser
+      delete parser;
     }
-    // Remove the parser
-    delete parser;
-  }
 
-  if( opts[options::replayStream] != NULL ) {
-    // this deletes the expression parser too
-    delete opts[options::replayStream];
-    opts.set(options::replayStream, NULL);
-  }
+    if( opts[options::replayStream] != NULL ) {
+      // this deletes the expression parser too
+      delete opts[options::replayStream];
+      opts.set(options::replayStream, NULL);
+    }
 
-  int returnValue;
-  string result = "unknown";
-  if(status) {
-    result = cmdExecutor.getSmtEngineStatus();
+    string result = "unknown";
+    if(status) {
+      result = pExecutor->getSmtEngineStatus();
 
-    if(result == "sat") {
-      returnValue = 10;
-    } else if(result == "unsat") {
-      returnValue = 20;
+      if(result == "sat") {
+        returnValue = 10;
+      } else if(result == "unsat") {
+        returnValue = 20;
+      } else {
+        returnValue = 0;
+      }
     } else {
-      returnValue = 0;
+      // there was some kind of error
+      returnValue = 1;
     }
-  } else {
-    // there was some kind of error
-    returnValue = 1;
-  }
 
 #ifdef CVC4_COMPETITION_MODE
-  // exit, don't return (don't want destructors to run)
-  // _exit() from unistd.h doesn't run global destructors
-  // or other on_exit/atexit stuff.
-  _exit(returnValue);
+    // exit, don't return (don't want destructors to run)
+    // _exit() from unistd.h doesn't run global destructors
+    // or other on_exit/atexit stuff.
+    _exit(returnValue);
 #endif /* CVC4_COMPETITION_MODE */
 
-  ReferenceStat< Result > s_statSatResult("sat/unsat", result);
-  RegisterStatistic statSatResultReg(&cmdExecutor.getStatisticsRegistry(), &s_statSatResult);
+    ReferenceStat< Result > s_statSatResult("sat/unsat", result);
+    RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(), &s_statSatResult);
 
-  s_totalTime.stop();
+    s_totalTime.stop();
 
-  // Set the global executor pointer to NULL first.  If we get a
-  // signal while dumping statistics, we don't want to try again.
-  pExecutor = NULL;
-  if(opts[options::statistics]) {
-    cmdExecutor.flushStatistics(*opts[options::err]);
-  }
+    // Set the global executor pointer to NULL first.  If we get a
+    // signal while dumping statistics, we don't want to try again.
+    if(opts[options::statistics]) {
+      pExecutor->flushStatistics(*opts[options::err]);
+    }
 
 #ifdef CVC4_DEBUG
-  if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
-    _exit(returnValue);
-  }
+    if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
+      _exit(returnValue);
+    }
 #else /* CVC4_DEBUG */
-  if(opts[options::earlyExit]) {
-    _exit(returnValue);
-  }
+    if(opts[options::earlyExit]) {
+      _exit(returnValue);
+    }
 #endif /* CVC4_DEBUG */
+  }
+
+  // On exceptional exit, these are leaked, but that's okay... they
+  // need to be around in that case for main() to print statistics.
+  delete pExecutor;
+  delete exprMgr;
+
+  pExecutor = NULL;
 
   return returnValue;
 }

diff --git a/src/options/mkoptions b/src/options/mkoptions
index 79ef35f5b0e8df1a19054342c0518735ff03c859..ffaff99279e05d1af8de013908c977aca9067fcf 100755 (executable)
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -852,6 +852,8 @@ function handle_alias {
         # false positive: =SOMETHING, where SOMETHING != ARG
         linkarg=
       fi
+    else
+      linkarg=
     fi
     links="$links
 #line $lineno \"$kf\"