From: Brian Norris Date: Fri, 15 Feb 2013 19:02:05 +0000 (-0800) Subject: model: fix leaking "pending actions" X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=fcae856e66379752f8d227784d28c424206ab0c1;p=cdsspec-compiler.git model: fix leaking "pending actions" ModelActions that are "pending" for each thread are not automatically freed when we rollback; we keep most of the active ModelActions on the NodeStack, then we free them from there when we explore a new branch of the state space. This fix causes all the pending actions to be freed on any rollback. This is safe for now, since we always roll back to the beginning of the execution. If we roll back to an intermediate point, though, we need to retain those pending actions which were also pending before the rollback point. Hence the FIXME notice included in reset_to_initial_state(). --- diff --git a/model.cc b/model.cc index 01e4c49..503253a 100644 --- a/model.cc +++ b/model.cc @@ -159,6 +159,14 @@ void ModelChecker::reset_to_initial_state() /* Print all model-checker output before rollback */ fflush(model_out); + /** + * FIXME: if we utilize partial rollback, we will need to free only + * those pending actions which were NOT pending before the rollback + * point + */ + for (unsigned int i = 0; i < get_num_threads(); i++) + delete get_thread(int_to_id(i))->get_pending(); + snapshot_backtrack_before(0); }