projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
9b5fe3a
)
Fix bug Weiyu found
author
root
<root@plrg-1.ics.uci.edu>
Fri, 20 Dec 2019 06:40:53 +0000
(22:40 -0800)
committer
root
<root@plrg-1.ics.uci.edu>
Fri, 20 Dec 2019 06:40:53 +0000
(22:40 -0800)
model.cc
patch
|
blob
|
history
model.h
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 7ae63b69334c1a35faae4d94a4dde0fcf5be4c7b..4f8a03243161ec61aa25644159c9856ae01188f8 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-30,7
+30,6
@@
void placeholder(void *) {
ModelChecker::ModelChecker() :
/* Initialize default scheduler */
params(),
ModelChecker::ModelChecker() :
/* Initialize default scheduler */
params(),
- restart_flag(false),
scheduler(new Scheduler()),
history(new ModelHistory()),
execution(new ModelExecution(this, scheduler)),
scheduler(new Scheduler()),
history(new ModelHistory()),
execution(new ModelExecution(this, scheduler)),
@@
-237,7
+236,7
@@
void ModelChecker::print_execution(bool printbugs) const
* @return If there are more executions to explore, return true. Otherwise,
* return false.
*/
* @return If there are more executions to explore, return true. Otherwise,
* return false.
*/
-
bool ModelChecker::next_execution(
)
+
void ModelChecker::finish_execution(bool more_executions
)
{
DBG();
/* Is this execution a feasible execution that's worth bug-checking? */
{
DBG();
/* Is this execution a feasible execution that's worth bug-checking? */
@@
-259,15
+258,11
@@
bool ModelChecker::next_execution()
else
clear_program_output();
else
clear_program_output();
- if (restart_flag) {
- do_restart();
- return true;
- }
// test code
execution_number ++;
// test code
execution_number ++;
- reset_to_initial_state();
+ if (more_executions)
+ reset_to_initial_state();
history->set_new_exec_flag();
history->set_new_exec_flag();
- return false;
}
/** @brief Run trace analyses on complete trace */
}
/** @brief Run trace analyses on complete trace */
@@
-371,21
+366,6
@@
bool ModelChecker::should_terminate_execution()
return false;
}
return false;
}
-/** @brief Restart ModelChecker upon returning to the run loop of the
- * model checker. */
-void ModelChecker::restart()
-{
- restart_flag = true;
-}
-
-void ModelChecker::do_restart()
-{
- restart_flag = false;
- reset_to_initial_state();
- memset(&stats,0,sizeof(struct execution_stats));
- execution_number = 1;
-}
-
/** @brief Run ModelChecker for the user program */
void ModelChecker::run()
{
/** @brief Run ModelChecker for the user program */
void ModelChecker::run()
{
@@
-472,7
+452,7
@@
void ModelChecker::run()
t->set_pending(NULL);
t = execution->take_step(curr);
} while (!should_terminate_execution());
t->set_pending(NULL);
t = execution->take_step(curr);
} while (!should_terminate_execution());
-
next_execution(
);
+
finish_execution((exec+1) < params.maxexecutions
);
//restore random number generator state after rollback
setstate(random_state);
}
//restore random number generator state after rollback
setstate(random_state);
}
diff --git
a/model.h
b/model.h
index c5a5aa78647deb2bfdb3ae7cf269b972ae5f89f0..62b227e4bcdce915125e9c8b7f9a877c94ee9529 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-35,9
+35,6
@@
public:
model_params * getParams();
void run();
model_params * getParams();
void run();
- /** Restart the model checker, intended for pluggins. */
- void restart();
-
/** Exit the model checker, intended for pluggins. */
void exit_model_checker();
/** Exit the model checker, intended for pluggins. */
void exit_model_checker();
@@
-69,9
+66,6
@@
public:
Scheduler * getScheduler() {return scheduler;}
MEMALLOC
private:
Scheduler * getScheduler() {return scheduler;}
MEMALLOC
private:
- /** Flag indicates whether to restart the model checker. */
- bool restart_flag;
-
/** Snapshot id we return to restart. */
snapshot_id snapshot;
/** Snapshot id we return to restart. */
snapshot_id snapshot;
@@
-85,7
+79,7
@@
private:
unsigned int get_num_threads() const;
unsigned int get_num_threads() const;
-
bool next_execution(
);
+
void finish_execution(bool moreexecutions
);
bool should_terminate_execution();
Thread * get_next_thread();
bool should_terminate_execution();
Thread * get_next_thread();
@@
-95,8
+89,6
@@
private:
ModelVector<TraceAnalysis *> trace_analyses;
ModelVector<TraceAnalysis *> trace_analyses;
- /** @bref Implement restart. */
- void do_restart();
/** @bref Plugin that can inspect new actions. */
TraceAnalysis *inspect_plugin;
/** @brief The cumulative execution stats */
/** @bref Plugin that can inspect new actions. */
TraceAnalysis *inspect_plugin;
/** @brief The cumulative execution stats */