#include "datarace.h"
#include "threads-model.h"
#include "output.h"
+#include "traceanalysis.h"
#define INITIAL_THREAD_ID 0
thrd_last_action(new SnapVector<ModelAction *>(1)),
thrd_last_fence_release(new SnapVector<ModelAction *>()),
node_stack(new NodeStack()),
+ trace_analyses(new ModelVector<Trace_Analysis *>()),
priv(new struct model_snapshot_members()),
mo_graph(new CycleGraph())
{
delete thrd_last_action;
delete thrd_last_fence_release;
delete node_stack;
+ for (unsigned int i = 0; i <trace_analyses->size();i++)
+ delete (*trace_analyses)[i];
+ delete trace_analyses;
delete scheduler;
delete mo_graph;
delete priv;
return tmp;
}
+action_list_t * ModelChecker::get_actions_on_obj(void * obj, thread_id_t tid) {
+ SnapVector<action_list_t> *wrv=obj_thrd_map->get(obj);
+ if (wrv==NULL)
+ return NULL;
+ unsigned int thread=id_to_int(tid);
+ if (thread < wrv->size())
+ return &(*wrv)[thread];
+ else
+ return NULL;
+}
+
+
/**
* Restores user program to initial state and resets all model-checker data
* structures.
assert_bug("Deadlock detected");
checkDataRaces();
+ run_trace_analyses();
}
record_stats();
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(action_trace);
+ }
+}
+
/**
* @brief Find the last fence-related backtracking conflict for a ModelAction
*