params: add multi-level verbosity

Now we can have --verbose=[012], so that the default (0) is still quiet,
the easy verbose flag (--verbose or -v) is noisy but useful (1), and if
you really want some extra noise, you can choose (2). Right now, there
is some minimal extra noise in (2), but this may be expanded if we want
more run-time debuggability, rather than recompiling with 'make debug'.

diff --git a/main.cc b/main.cc
index 32c153da565d209d4397fccd9148c96819d177d8..8416a79c88db8b35b5d706413d36da8160b3afc0 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -75,7 +75,9 @@ static void print_usage(const char *program_name, struct model_params *params)
 "                              Default: %d\n"
 "-b, --bound=MAX             Upper length bound.\n"
 "                              Default: %d\n"
-"-v, --verbose               Print verbose execution information.\n"
+"-v[NUM], --verbose[=NUM]    Print verbose execution information. NUM is optional:\n"
+"                              0 is quiet; 1 is noisy; 2 is noisier.\n"
+"                              Default: %d\n"
 "-u, --uninitialized=VALUE   Return VALUE any load which may read from an\n"
 "                              uninitialized atomic.\n"
 "                              Default: %u\n"
@@ -93,6 +95,7 @@ static void print_usage(const char *program_name, struct model_params *params)
                params->fairwindow,
                params->enabledcount,
                params->bound,
+               params->verbose,
                params->uninitvalue);
        model_print("Analysis plugins:\n");
        for(unsigned int i=0;i<registeredanalysis->size();i++) {

diff --git a/model.cc b/model.cc
index 90ef906ef6348ed9cdfc6717c1eaab1fb3d9e886..466bf613a905ece97aaba98c506e1bf9234109e7 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -254,7 +254,7 @@ void ModelChecker::print_execution(bool printbugs) const
 {
        print_program_output();
 
-       if (params.verbose) {
+       if (params.verbose >= 2) {
                model_print("Earliest divergence point since last feasible execution:\n");
                if (earliest_diverge)
                        earliest_diverge->print();

diff --git a/params.h b/params.h
index 0eda8bfa562e281a7bf1e93ae4f565c0449da455..ac5dd9665b6a2cf5e66b276668bb127eb98e4230 100644 (file)
--- a/params.h
+++ b/params.h
@@ -24,7 +24,7 @@ struct model_params {
         *  value */
        unsigned int expireslop;
 
-       /** @brief Verbosity (0 = quiet; 1 = noisy) */
+       /** @brief Verbosity (0 = quiet; 1 = noisy; 2 = noisier) */
        int verbose;
 
        /** @brief Command-line argument count to pass to user program */