diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-04 03:31:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-04 03:31:38 +0000 |
commit | fc14c009e8e9d2274368b54c12f3580a9ec8f718 (patch) | |
tree | 853fdc64b8f6f29dc106e581dfe8ed8e4c569778 /src/main | |
parent | 33988bd64b92960f7bed5c68d1266adc4183454b (diff) |
src/expr/kind.h is now automatically generated.
Build src/expr before src/util.
Moved CVC4::Command to the expr package.
Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).
Added file-level documentation to Antlr sources
When built for debug, spin on SEGV instead of aborting. Really useful
for debugging problems that crop up only on long runs. Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.
Updated src/main/about.h for 2010.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/about.h | 8 | ||||
-rw-r--r-- | src/main/getopt.cpp | 45 | ||||
-rw-r--r-- | src/main/main.cpp | 2 | ||||
-rw-r--r-- | src/main/main.h | 21 | ||||
-rw-r--r-- | src/main/usage.h | 4 | ||||
-rw-r--r-- | src/main/util.cpp | 28 |
6 files changed, 84 insertions, 24 deletions
diff --git a/src/main/about.h b/src/main/about.h index d00b1eaec..a30cffd39 100644 --- a/src/main/about.h +++ b/src/main/about.h @@ -21,9 +21,11 @@ namespace main { const char about[] = "\ This is a pre-release of CVC4.\n\ -Copyright (C) 2009 The ACSys Group\n\ - Courant Institute of Mathematical Sciences,\n\ - New York University\n\ +Copyright (C) 2009, 2010\n\ + The ACSys Group\n\ + Courant Institute of Mathematical Sciences,\n\ + New York University\n\ + New York, NY 10012 USA\n\ "; }/* CVC4::main namespace */ diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 6eb70a3e1..f4d32cd68 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -56,25 +56,35 @@ CNF conversions currently supported as arguments to the --cnf option:\n\ enum OptionValue { CNF = 256, /* no clash with char options */ SMTCOMP, - STATS + STATS, + SEGV_NOSPIN };/* enum OptionValue */ // FIXME add a comment here describing the option array static struct option cmdlineOptions[] = { // name, has_arg, *flag, val - { "help" , no_argument , NULL, 'h' }, - { "version", no_argument , NULL, 'V' }, - { "verbose", no_argument , NULL, 'v' }, - { "quiet" , no_argument , NULL, 'q' }, - { "lang" , required_argument, NULL, 'L' }, - { "debug" , required_argument, NULL, 'd' }, - { "cnf" , required_argument, NULL, CNF }, - { "smtcomp", no_argument , NULL, SMTCOMP }, - { "stats" , no_argument , NULL, STATS } + { "help" , no_argument , NULL, 'h' }, + { "version" , no_argument , NULL, 'V' }, + { "verbose" , no_argument , NULL, 'v' }, + { "quiet" , no_argument , NULL, 'q' }, + { "lang" , required_argument, NULL, 'L' }, + { "debug" , required_argument, NULL, 'd' }, + { "cnf" , required_argument, NULL, CNF }, + { "smtcomp" , no_argument , NULL, SMTCOMP }, + { "stats" , no_argument , NULL, STATS }, + { "segv-nospin", no_argument , NULL, SEGV_NOSPIN } };/* if you add things to the above, please remember to update usage.h! */ -int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionException) { - const char *progName = argv[0]; +/** Full argv[0] */ +const char *progPath; + +/** Just the basename component of argv[0] */ +const char *progName; + +/** Parse argc/argv and put the result into a CVC4::Options struct. */ +int parseOptions(int argc, char** argv, CVC4::Options* opts) +throw(OptionException) { + progPath = progName = argv[0]; int c; // find the base name of the program @@ -85,17 +95,18 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti opts->binary_name = string(progName); // FIXME add a comment here describing the option string - while((c = getopt_long(argc, argv, "+:hVvqL:d:", cmdlineOptions, NULL)) != -1) { + while((c = getopt_long(argc, argv, + "+:hVvqL:d:", + cmdlineOptions, NULL)) != -1) { switch(c) { case 'h': printf(usage, opts->binary_name.c_str()); exit(1); - break; case 'V': fputs(about, stdout); - break; + exit(0); case 'v': ++opts->verbosity; @@ -148,6 +159,10 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti opts->statistics = true; break; + case SEGV_NOSPIN: + segvNoSpin = true; + break; + case SMTCOMP: // silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input) opts->smtcomp_mode = true; diff --git a/src/main/main.cpp b/src/main/main.cpp index 02ebe8deb..de179edb8 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -25,7 +25,7 @@ #include "parser/parser.h" #include "expr/expr_manager.h" #include "smt/smt_engine.h" -#include "util/command.h" +#include "expr/command.h" #include "util/result.h" #include "util/Assert.h" #include "util/output.h" diff --git a/src/main/main.h b/src/main/main.h index 9b2f4fcbe..0c78912ae 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -28,12 +28,31 @@ struct Options; namespace main { +/** Class representing an option-parsing exception. */ class OptionException : public CVC4::Exception { public: - OptionException(const std::string& s) throw() : CVC4::Exception("Error in option parsing: " + s) {} + OptionException(const std::string& s) throw() : + CVC4::Exception("Error in option parsing: " + s) { + } };/* class OptionException */ +/** Full argv[0] */ +extern const char *progPath; + +/** Just the basename component of argv[0] */ +extern const char *progName; + +/** + * If true, will not spin on segfault even when CVC4_DEBUG is on. + * Useful for nightly regressions, noninteractive performance runs + * etc. See util.cpp. + */ +extern bool segvNoSpin; + +/** Parse argc/argv and put the result into a CVC4::Options struct. */ int parseOptions(int argc, char** argv, CVC4::Options*) throw(OptionException); + +/** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ void cvc4_init() throw(); }/* CVC4::main namespace */ diff --git a/src/main/usage.h b/src/main/usage.h index f6c089f1d..6927f0f2f 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -27,8 +27,7 @@ usage: %s [options] [input-file]\n\ Without an input file, or with `-', CVC4 reads from standard input.\n\ \n\ CVC4 options:\n\ - --lang | -L set input language (--lang help gives a list;\n\ - `auto' is default)\n\ + --lang | -L force input language (default is `auto'; see --lang help)\n\ --version | -V identify this CVC4 binary\n\ --help | -h this command line reference\n\ --verbose | -v increase verbosity (repeatable)\n\ @@ -36,6 +35,7 @@ CVC4 options:\n\ --debug | -d debugging for something (e.g. --debug arith)\n\ --smtcomp competition mode (very quiet)\n\ --stats give statistics on exit\n\ + --segv-nospin (debug builds only) don't spin on segfault waiting for gdb\n\ "; }/* CVC4::main namespace */ diff --git a/src/main/util.cpp b/src/main/util.cpp index df4ab803d..03ae26092 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -10,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** [[ Add file-specific comments here ]] + ** Utilities for the main driver. **/ #include <cstdio> @@ -22,24 +22,48 @@ #include "util/exception.h" #include "config.h" +#include "main.h" + using CVC4::Exception; using namespace std; namespace CVC4 { namespace main { -// FIXME add comments to functions +/** + * If true, will not spin on segfault even when CVC4_DEBUG is on. + * Useful for nightly regressions, noninteractive performance runs + * etc. + */ +bool segvNoSpin = false; +/** Handler for SIGINT, i.e., when the user hits control C. */ void sigint_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by user.\n"); abort(); } +/** Handler for SIGSEGV (segfault). */ void segv_handler(int sig, siginfo_t* info, void*) { +#ifdef CVC4_DEBUG + fprintf(stderr, "CVC4 suffered a segfault in DEBUG mode.\n"); + if(segvNoSpin) { + fprintf(stderr, "No-spin requested, aborting...\n"); + abort(); + } else { + fprintf(stderr, "Spinning so that a debugger can be connected.\n"); + fprintf(stderr, "Try: gdb %s %u\n", progName, getpid()); + for(;;) { + sleep(60); + } + } +#else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 suffered a segfault.\n"); abort(); +#endif /* CVC4_DEBUG */ } +/** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ void cvc4_init() throw() { struct sigaction act1; act1.sa_sigaction = sigint_handler; |