* @param msg Descriptive message for the bug (do not include newline char)
* @return True if bug is immediately-feasible
*/
-bool ModelChecker::assert_bug(const char *msg, ...)
+void ModelChecker::assert_bug(const char *msg, ...)
{
char str[800];
vsnprintf(str, sizeof(str), msg, ap);
va_end(ap);
- return execution->assert_bug(str);
+ execution->assert_bug(str);
}
/**
void ModelChecker::assert_user_bug(const char *msg)
{
/* If feasible bug, bail out now */
- if (assert_bug(msg))
- switch_to_master(NULL);
+ assert_bug(msg);
+ switch_to_master(NULL);
}
/** @brief Print bug report listing for this execution (if any bugs exist) */
void ModelChecker::record_stats()
{
stats.num_total ++;
- if (!execution->isfeasibleprefix())
- stats.num_infeasible ++;
- else if (execution->have_bug_reports())
+ if (execution->have_bug_reports())
stats.num_buggy_executions ++;
else if (execution->is_complete_execution())
stats.num_complete ++;
else {
- stats.num_redundant ++;
-
+ //All threads are sleeping
/**
* @todo We can violate this ASSERT() when fairness/sleep sets
* conflict to cause an execution to terminate, e.g. with:
void ModelChecker::print_stats() const
{
model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
- model_print("Number of redundant executions: %d\n", stats.num_redundant);
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);
}
{
DBG();
/* Is this execution a feasible execution that's worth bug-checking? */
- bool complete = execution->isfeasibleprefix() &&
- (execution->is_complete_execution() ||
+ bool complete = (execution->is_complete_execution() ||
execution->have_bug_reports());
/* End-of-execution bug checks */
bool ModelChecker::should_terminate_execution()
{
- /* Infeasible -> don't take any more steps */
- if (execution->is_infeasible())
- return true;
- else if (execution->isfeasibleprefix() && execution->have_bug_reports()) {
+ if (execution->have_bug_reports()) {
execution->set_assert();
return true;
} else if (execution->isFinished()) {
if (t->just_woken_up()) {
t->set_wakeup_state(false);
t->set_pending(NULL);
+ t = NULL;
continue; // Allow this thread to stash the next pending action
}