From 65e1c44cb1a70d7d19bc32b07bf41a7a6fa722d0 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 10 Jan 2013 10:54:02 -0800 Subject: [PATCH] model: reformat execution trace prints Bring the "INFEASIBLE" message together with the "Execution #" message, to make the log more compact and readable (e.g., grep for "Execution" will give you some regularly-patterned, useful information). --- model.cc | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/model.cc b/model.cc index c63d9d9..9c34884 100644 --- a/model.cc +++ b/model.cc @@ -2576,13 +2576,11 @@ ModelAction * ModelChecker::new_uninitialized_action(void *location) const return act; } -static void print_list(action_list_t *list, int exec_num = -1) +static void print_list(action_list_t *list) { action_list_t::iterator it; model_print("---------------------------------------------------------------------\n"); - if (exec_num >= 0) - model_print("Execution %d:\n", exec_num); unsigned int hash = 0; @@ -2635,9 +2633,12 @@ void ModelChecker::print_summary() const dumpGraph(buffername); #endif - if (!isfeasibleprefix()) - print_infeasibility("INFEASIBLE EXECUTION"); - print_list(action_trace, stats.num_total); + model_print("Execution %d:", stats.num_total); + if (isfeasibleprefix()) + model_print("\n"); + else + print_infeasibility(" INFEASIBLE"); + print_list(action_trace); model_print("\n"); } -- 2.34.1