#include "threads-model.h"
#include "output.h"
#include "traceanalysis.h"
+#include "bugmessage.h"
#define INITIAL_THREAD_ID 0
ModelChecker *model;
-struct bug_message {
- bug_message(const char *str) {
- const char *fmt = " [BUG] %s\n";
- msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
- sprintf(msg, fmt, str);
- }
- ~bug_message() { if (msg) snapshot_free(msg); }
-
- char *msg;
- void print() { model_print("%s", msg); }
-
- SNAPSHOTALLOC
-};
-
/**
* Structure for holding small ModelChecker members that should be snapshotted
*/
thrd_last_action(new SnapVector<ModelAction *>(1)),
thrd_last_fence_release(new SnapVector<ModelAction *>()),
node_stack(new NodeStack()),
- trace_analyses(new ModelVector<Trace_Analysis *>()),
+ trace_analyses(new ModelVector<TraceAnalysis *>()),
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++)
+ for (unsigned int i = 0; i < trace_analyses->size(); i++)
delete (*trace_analyses)[i];
delete trace_analyses;
delete scheduler;
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.
return true;
}
-/**
- * @brief Run trace analyses on complete trace. */
-
+/** @brief Run trace analyses on complete trace */
void ModelChecker::run_trace_analyses() {
- for(unsigned int i=0; i < trace_analyses->size(); i++) {
+ for (unsigned int i = 0; i < trace_analyses->size(); i++)
(*trace_analyses)[i]->analyze(action_trace);
- }
}
/**
user_main(model->params.argc, model->params.argv);
}
+/** @return True if the execution has taken too many steps */
+bool ModelChecker::too_many_steps() const
+{
+ return params.bound != 0 && priv->used_sequence_numbers > params.bound;
+}
+
bool ModelChecker::should_terminate_execution()
{
/* Infeasible -> don't take any more steps */
return true;
}
- if (params.bound != 0 && priv->used_sequence_numbers > params.bound)
+ if (too_many_steps())
return true;
return false;
}