~bug_message() { if (msg) snapshot_free(msg); }
char *msg;
- void print() { printf("%s", msg); }
+ void print() { model_print("%s", msg); }
SNAPSHOTALLOC
};
void ModelChecker::print_bugs() const
{
if (have_bug_reports()) {
- printf("Bug report: %zu bugs detected\n", priv->bugs.size());
+ model_print("Bug report: %zu bug%s detected\n",
+ priv->bugs.size(),
+ priv->bugs.size() > 1 ? "s" : "");
for (unsigned int i = 0; i < priv->bugs.size(); i++)
priv->bugs[i]->print();
}
/** @brief Print execution stats */
void ModelChecker::print_stats() const
{
- printf("Number of complete, bug-free executions: %d\n", stats.num_complete);
- printf("Number of buggy executions: %d\n", stats.num_buggy_executions);
- printf("Number of infeasible executions: %d\n", stats.num_infeasible);
- printf("Total executions: %d\n", stats.num_total);
- printf("Total nodes created: %d\n", node_stack->get_total_nodes());
+ model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
+ 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);
+ model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
}
/**
{
DBG();
- record_stats();
-
if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
- printf("Earliest divergence point since last feasible execution:\n");
+ model_print("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
earliest_diverge->print();
else
- printf("(Not set)\n");
+ model_print("(Not set)\n");
earliest_diverge = NULL;
checkDataRaces();
print_bugs();
- printf("\n");
- print_stats();
+ model_print("\n");
print_summary();
} else if (DBG_ENABLED()) {
- printf("\n");
+ model_print("\n");
print_summary();
}
+ record_stats();
+
if ((diverge = get_next_backtrack()) == NULL)
return false;
if (DBG_ENABLED()) {
- printf("Next execution will diverge at:\n");
+ model_print("Next execution will diverge at:\n");
diverge->print();
}
assert_bug("May read from uninitialized atomic");
if (DBG_ENABLED() || !initialized) {
- printf("Reached read action:\n");
+ model_print("Reached read action:\n");
curr->print();
- printf("Printing may_read_from\n");
+ model_print("Printing may_read_from\n");
curr->get_node()->print_may_read_from();
- printf("End printing may_read_from\n");
+ model_print("End printing may_read_from\n");
}
}
}
}
-static void print_list(action_list_t *list)
+static void print_list(action_list_t *list, int exec_num = -1)
{
action_list_t::iterator it;
- printf("---------------------------------------------------------------------\n");
- printf("Trace:\n");
+ model_print("---------------------------------------------------------------------\n");
+ if (exec_num >= 0)
+ model_print("Execution %d:\n", exec_num);
+
unsigned int hash=0;
for (it = list->begin(); it != list->end(); it++) {
(*it)->print();
hash=hash^(hash<<3)^((*it)->hash());
}
- printf("HASH %u\n", hash);
- printf("---------------------------------------------------------------------\n");
+ model_print("HASH %u\n", hash);
+ model_print("---------------------------------------------------------------------\n");
}
#if SUPPORT_MOD_ORDER_DUMP
#endif
if (!isfinalfeasible())
- printf("INFEASIBLE EXECUTION!\n");
- print_list(action_trace);
- printf("\n");
+ model_print("INFEASIBLE EXECUTION!\n");
+ print_list(action_trace, stats.num_total);
+ model_print("\n");
}
/**
*/
if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
isfinalfeasible() && !unrealizedraces.empty()) {
- printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
+ model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
pending_rel_seqs->size());
ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
std::memory_order_seq_cst, NULL, VALUE_NONE,