stats.num_buggy_executions++;
else if (is_complete_execution())
stats.num_complete++;
+ else
+ stats.num_redundant++;
}
/** @brief Print execution stats */
void ModelChecker::print_stats() const
{
model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
+ model_print("Number of redundant executions: %d\n", stats.num_redundant);
model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
model_print("Total executions: %d\n", stats.num_total);
}
/**
- * Queries the model-checker for more executions to explore and, if one
- * exists, resets the model-checker state to execute a new execution.
- *
- * @return If there are more executions to explore, return true. Otherwise,
- * return false.
+ * @brief End-of-exeuction print
+ * @param printbugs Should any existing bugs be printed?
*/
-bool ModelChecker::next_execution()
+void ModelChecker::print_execution(bool printbugs) const
{
- DBG();
+ print_program_output();
- if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
+ if (DBG_ENABLED() || params.verbose) {
model_print("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
earliest_diverge->print();
else
model_print("(Not set)\n");
- earliest_diverge = NULL;
+ model_print("\n");
+ print_stats();
+ }
+
+ /* Don't print invalid bugs */
+ if (printbugs)
+ print_bugs();
+
+ model_print("\n");
+ print_summary();
+}
+
+/**
+ * Queries the model-checker for more executions to explore and, if one
+ * exists, resets the model-checker state to execute a new execution.
+ *
+ * @return If there are more executions to explore, return true. Otherwise,
+ * return false.
+ */
+bool ModelChecker::next_execution()
+{
+ DBG();
+ /* Is this execution a feasible execution that's worth bug-checking? */
+ bool complete = isfinalfeasible() && (is_complete_execution() ||
+ have_bug_reports());
+ /* End-of-execution bug checks */
+ if (complete) {
if (is_deadlocked())
assert_bug("Deadlock detected");
checkDataRaces();
- print_bugs();
- model_print("\n");
- print_summary();
- } else if (DBG_ENABLED()) {
- model_print("\n");
- print_summary();
}
record_stats();
+ /* Output */
+ if (DBG_ENABLED() || params.verbose || have_bug_reports())
+ print_execution(complete);
+ else
+ clear_program_output();
+
+ if (complete)
+ earliest_diverge = NULL;
+
if ((diverge = get_next_backtrack()) == NULL)
return false;
}
#endif
-void ModelChecker::print_summary()
+/** @brief Prints an execution trace summary. */
+void ModelChecker::print_summary() const
{
#if SUPPORT_MOD_ORDER_DUMP
scheduler->print();