projects
/
c11tester.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
initialize the newly added element in the vector when resizing func_nodes
[c11tester.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index b8d9f7cb4ce46b7c01ed7aa08fe982985a7a9cd0..45fa1b20ff11462c7999090a34e34f31212b049d 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-7,7
+7,6
@@
#include "model.h"
#include "action.h"
#include "model.h"
#include "action.h"
-#include "nodestack.h"
#include "schedule.h"
#include "snapshot-interface.h"
#include "common.h"
#include "schedule.h"
#include "snapshot-interface.h"
#include "common.h"
@@
-34,8
+33,7
@@
ModelChecker::ModelChecker() :
params(),
restart_flag(false),
scheduler(new Scheduler()),
params(),
restart_flag(false),
scheduler(new Scheduler()),
- node_stack(new NodeStack()),
- execution(new ModelExecution(this, scheduler, node_stack)),
+ execution(new ModelExecution(this, scheduler)),
history(new ModelHistory()),
execution_number(1),
trace_analyses(),
history(new ModelHistory()),
execution_number(1),
trace_analyses(),
@@
-47,12
+45,12
@@
ModelChecker::ModelChecker() :
scheduler->set_current_thread(init_thread);
execution->setParams(¶ms);
param_defaults(¶ms);
scheduler->set_current_thread(init_thread);
execution->setParams(¶ms);
param_defaults(¶ms);
+ initRaceDetector();
}
/** @brief Destructor */
ModelChecker::~ModelChecker()
{
}
/** @brief Destructor */
ModelChecker::~ModelChecker()
{
- delete node_stack;
delete scheduler;
}
delete scheduler;
}
@@
-114,7
+112,7
@@
Thread * ModelChecker::get_next_thread()
* Have we completed exploring the preselected path? Then let the
* scheduler decide
*/
* Have we completed exploring the preselected path? Then let the
* scheduler decide
*/
- return scheduler->select_next_thread(
node_stack->get_head()
);
+ return scheduler->select_next_thread();
}
/**
}
/**
@@
-246,7
+244,6
@@
bool ModelChecker::next_execution()
if (execution->is_deadlocked())
assert_bug("Deadlock detected");
if (execution->is_deadlocked())
assert_bug("Deadlock detected");
- checkDataRaces();
run_trace_analyses();
}
run_trace_analyses();
}
@@
-319,6
+316,16
@@
void ModelChecker::switch_from_master(Thread *thread)
*/
uint64_t ModelChecker::switch_to_master(ModelAction *act)
{
*/
uint64_t ModelChecker::switch_to_master(ModelAction *act)
{
+ if (forklock) {
+ static bool fork_message_printed = false;
+
+ if (!fork_message_printed) {
+ model_print("Fork handler trying to call into model checker...\n");
+ fork_message_printed = true;
+ }
+ delete act;
+ return 0;
+ }
DBG();
Thread *old = thread_current();
scheduler->set_current_thread(NULL);
DBG();
Thread *old = thread_current();
scheduler->set_current_thread(NULL);
@@
-350,7
+357,7
@@
bool ModelChecker::should_terminate_execution()
/* Infeasible -> don't take any more steps */
if (execution->is_infeasible())
return true;
/* Infeasible -> don't take any more steps */
if (execution->is_infeasible())
return true;
- else if (execution->isfeasibleprefix() && execution->have_bug_reports()) {
+ else if (execution->isfeasibleprefix() && execution->have_
fatal_
bug_reports()) {
execution->set_assert();
return true;
}
execution->set_assert();
return true;
}