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 01e4c491a9e637cb1c1ffd2b78607c82f2472e82..503253af17a5dc0ba4727b3dcff08d1dfcbf07d2 100644 (file)
--- 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);
 }