X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=466bf613a905ece97aaba98c506e1bf9234109e7;hb=251c63183adee7dbdceeabce5a706e8281bc2887;hp=55949730f5c2a00428618dd8cfbe8bf65c96747f;hpb=a22d12cff31e5309eb0033324d3dd0258de53cb5;p=c11tester.git diff --git a/model.cc b/model.cc index 55949730..466bf613 100644 --- a/model.cc +++ b/model.cc @@ -1,6 +1,5 @@ #include #include -#include #include #include @@ -17,8 +16,6 @@ #include "execution.h" #include "bugmessage.h" -#define INITIAL_THREAD_ID 0 - ModelChecker *model; /** @brief Constructor */ @@ -27,10 +24,11 @@ ModelChecker::ModelChecker(struct model_params params) : params(params), scheduler(new Scheduler()), node_stack(new NodeStack()), - execution(new ModelExecution(¶ms, scheduler, node_stack)), + execution(new ModelExecution(this, &this->params, scheduler, node_stack)), + execution_number(1), diverge(NULL), earliest_diverge(NULL), - trace_analyses(new ModelVector()) + trace_analyses() { } @@ -38,9 +36,6 @@ ModelChecker::ModelChecker(struct model_params params) : ModelChecker::~ModelChecker() { delete node_stack; - for (unsigned int i = 0; i < trace_analyses->size(); i++) - delete (*trace_analyses)[i]; - delete trace_analyses; delete scheduler; } @@ -259,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(); @@ -321,15 +316,16 @@ bool ModelChecker::next_execution() diverge->print(); } - execution->increment_execution_number(); + execution_number++; + reset_to_initial_state(); return true; } /** @brief Run trace analyses on complete trace */ void ModelChecker::run_trace_analyses() { - for (unsigned int i = 0; i < trace_analyses->size(); i++) - (*trace_analyses)[i]->analyze(execution->get_action_trace()); + for (unsigned int i = 0; i < trace_analyses.size(); i++) + trace_analyses[i]->analyze(execution->get_action_trace()); } /** @@ -436,7 +432,7 @@ void ModelChecker::run() { do { thrd_t user_thread; - Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL, NULL); + Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); execution->add_thread(t); do { @@ -446,7 +442,7 @@ void ModelChecker::run() * thread which just took a step--plus the first step * for any newly-created thread */ - for (unsigned int i = 0; i < execution->get_num_threads(); i++) { + for (unsigned int i = 0; i < get_num_threads(); i++) { thread_id_t tid = int_to_id(i); Thread *thr = get_thread(tid); if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) { @@ -487,4 +483,8 @@ void ModelChecker::run() model_print("******* Model-checking complete: *******\n"); print_stats(); + + /* Have the trace analyses dump their output. */ + for (unsigned int i = 0; i < trace_analyses.size(); i++) + trace_analyses[i]->finish(); }