model: cosmetic output improvements

A few cosmetic improvements:

* Provide more uniform newlines

* Clearly show which output is produced by the test program

* Provide clear heading to show which output belongs to which program
  execution

* Label the program trace if it has bugs

I'm sure there's more that could be improved, but that's it for now.

diff --git a/common.cc b/common.cc
index 66b563a8ba6223a32a2c7d08067406fec0914c4b..26f6d5d8cd42bdd28484c231a995b5fbe84c633b 100644 (file)
--- a/common.cc
+++ b/common.cc
@@ -147,6 +147,8 @@ void print_program_output()
 {
        char buf[200];
 
+       model_print("---- BEGIN PROGRAM OUTPUT ----\n");
+
        /* Gather all program output */
        fflush(stdout);
 
@@ -165,5 +167,7 @@ void print_program_output()
                        ret -= res;
                }
        }
+
+       model_print("---- END PROGRAM OUTPUT   ----\n");
 }
 #endif /* ! CONFIG_DEBUG */

diff --git a/execution.cc b/execution.cc
index 403d70fe06361f3959ed21a4b94654b5fc6b4c1a..07866fe804a308054c716ae4eb92ba146cd53e15 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -1389,7 +1389,7 @@ void ModelExecution::print_infeasibility(const char *prefix) const
        if (promises.size() != 0)
                ptr += sprintf(ptr, "[unresolved promise]");
        if (ptr != buf)
-               model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf);
+               model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
 }
 
 /**
@@ -2697,17 +2697,21 @@ void ModelExecution::print_summary() const
        dumpGraph(buffername);
 #endif
 
-       model_print("Execution %d:", get_execution_number());
+       model_print("Execution trace %d:", get_execution_number());
        if (isfeasibleprefix()) {
                if (is_yieldblocked())
                        model_print(" YIELD BLOCKED");
                if (scheduler->all_threads_sleeping())
                        model_print(" SLEEP-SET REDUNDANT");
-               model_print("\n");
+               if (have_bug_reports())
+                       model_print(" DETECTED BUG(S)");
        } else
                print_infeasibility(" INFEASIBLE");
+       model_print("\n");
+
        print_list(&action_trace);
        model_print("\n");
+
        if (!promises.empty()) {
                model_print("Pending promises:\n");
                for (unsigned int i = 0; i < promises.size(); i++) {

diff --git a/model.cc b/model.cc
index 466bf613a905ece97aaba98c506e1bf9234109e7..16d5db4ab280262d1c4439de6544a413f8ba794e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -197,15 +197,13 @@ void ModelChecker::assert_user_bug(const char *msg)
 /** @brief Print bug report listing for this execution (if any bugs exist) */
 void ModelChecker::print_bugs() const
 {
-       if (execution->have_bug_reports()) {
-               SnapVector<bug_message *> *bugs = execution->get_bugs();
-
-               model_print("Bug report: %zu bug%s detected\n",
-                               bugs->size(),
-                               bugs->size() > 1 ? "s" : "");
-               for (unsigned int i = 0; i < bugs->size(); i++)
-                       (*bugs)[i]->print();
-       }
+       SnapVector<bug_message *> *bugs = execution->get_bugs();
+
+       model_print("Bug report: %zu bug%s detected\n",
+                       bugs->size(),
+                       bugs->size() > 1 ? "s" : "");
+       for (unsigned int i = 0; i < bugs->size(); i++)
+               (*bugs)[i]->print();
 }
 
 /**
@@ -252,10 +250,12 @@ void ModelChecker::print_stats() const
  */
 void ModelChecker::print_execution(bool printbugs) const
 {
+       model_print("Program output from execution %d:\n",
+                       get_execution_number());
        print_program_output();
 
        if (params.verbose >= 2) {
-               model_print("Earliest divergence point since last feasible execution:\n");
+               model_print("\nEarliest divergence point since last feasible execution:\n");
                if (earliest_diverge)
                        earliest_diverge->print();
                else
@@ -266,8 +266,10 @@ void ModelChecker::print_execution(bool printbugs) const
        }
 
        /* Don't print invalid bugs */
-       if (printbugs)
+       if (printbugs && execution->have_bug_reports()) {
+               model_print("\n");
                print_bugs();
+       }
 
        model_print("\n");
        execution->print_summary();