From: Brian Norris <banorris@uci.edu>
Date: Fri, 31 May 2013 23:45:42 +0000 (-0700)
Subject: params: add multi-level verbosity
X-Git-Tag: oopsla2013~4
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=251c63183adee7dbdceeabce5a706e8281bc2887

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 32c153d..8416a79 100644
--- 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 90ef906..466bf61 100644
--- 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 0eda8bf..ac5dd96 100644
--- 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 */