model-checker : remove useless ignore

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index d034675..fc8cb90 100644 (file)
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -248,11 +248,6 @@ void MC_pre_modelcheck_comm_determinism(void)
   /* Wait for requests (schedules processes) */
   MC_wait_for_requests();
 
-  if (_sg_mc_visited > 0) {
-    MC_ignore_heap(simix_global->process_to_run->data, 0);
-    MC_ignore_heap(simix_global->process_that_ran->data, 0);
-  }
-
   MC_SET_MC_HEAP;
 
   /* Get an enabled process and insert it in the interleave set of the initial state */

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 72ab536..887aedc 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -278,14 +278,6 @@ void MC_init()
     MC_ignore_global_variable("maestro_stack_end");
     MC_ignore_global_variable("smx_total_comms");
 
-    MC_ignore_heap(&(simix_global->process_to_run),
-                   sizeof(simix_global->process_to_run));
-    MC_ignore_heap(&(simix_global->process_that_ran),
-                   sizeof(simix_global->process_that_ran));
-    MC_ignore_heap(simix_global->process_to_run,
-                   sizeof(*(simix_global->process_to_run)));
-    MC_ignore_heap(simix_global->process_that_ran,
-                   sizeof(*(simix_global->process_that_ran)));
     MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
 
     smx_process_t process;

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 2c5ded0..b45b279 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -216,9 +216,6 @@ void MC_pre_modelcheck_liveness(void)
 
   MC_wait_for_requests();
 
-  MC_ignore_heap(simix_global->process_to_run->data, 0);
-  MC_ignore_heap(simix_global->process_that_ran->data, 0);
-
   MC_SET_MC_HEAP;
 
   acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);

diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c
index 3c4f93f..d68a78b 100644 (file)
--- a/src/mc/mc_safety.c
+++ b/src/mc/mc_safety.c
@@ -45,11 +45,6 @@ void MC_pre_modelcheck_safety()
   /* Wait for requests (schedules processes) */
   MC_wait_for_requests();
 
-  if (_sg_mc_visited > 0) {
-    MC_ignore_heap(simix_global->process_to_run->data, 0);
-    MC_ignore_heap(simix_global->process_that_ran->data, 0);
-  }
-
   MC_SET_MC_HEAP;
 
   /* Get an enabled process and insert it in the interleave set of the initial state */