diff options
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/getopt.cpp | 14 | ||||
| -rw-r--r-- | src/main/usage.h | 3 |
2 files changed, 15 insertions, 2 deletions
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index cd952eef9..a272aaafd 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -81,6 +81,12 @@ enum OptionValue { * getopt_long() returns the 4th entry * 4. the return value for getopt_long() when this long option (or the * value to set the 3rd entry to; see #3) + * + * If you add something here, you should add it in src/main/usage.h + * also, to document it. + * + * If you add something that has a short option equivalent, you should + * add it to the getopt_long() call in parseOptions(). */ static struct option cmdlineOptions[] = { // name, has_arg, *flag, val @@ -91,6 +97,7 @@ static struct option cmdlineOptions[] = { { "quiet" , no_argument , NULL, 'q' }, { "lang" , required_argument, NULL, 'L' }, { "debug" , required_argument, NULL, 'd' }, + { "trace" , required_argument, NULL, 't' }, { "smtcomp" , no_argument , NULL, SMTCOMP }, { "stats" , no_argument , NULL, STATS }, { "segv-nospin", no_argument , NULL, SEGV_NOSPIN }, @@ -131,7 +138,7 @@ throw(OptionException) { // cmdlineOptions specifies all the long-options and the return // value for getopt_long() should they be encountered. while((c = getopt_long(argc, argv, - "+:hVvqL:d:", + "+:hVvqL:d:t:", cmdlineOptions, NULL)) != -1) { switch(c) { @@ -171,8 +178,13 @@ throw(OptionException) { fputs(lang_help, stdout); exit(1); + case 't': + Trace.on(optarg); + break; + case 'd': Debug.on(optarg); + Trace.on(optarg); /* fall-through */ case STATS: diff --git a/src/main/usage.h b/src/main/usage.h index 3a609d2ec..c8ca6a179 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -32,7 +32,8 @@ CVC4 options:\n\ --help | -h this command line reference\n\ --verbose | -v increase verbosity (repeatable)\n\ --quiet | -q decrease verbosity (repeatable)\n\ - --debug | -d debugging for something (e.g. --debug arith)\n\ + --trace | -t tracing for something (e.g. --trace pushpop)\n\ + --debug | -d debugging for something (e.g. --debug arith), implies -t\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\ |