X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ab23fd586c00bc3e9ea24f1dcd3d52dd0fc60bce..6479f2478ed2c405d6f97e6aa87799b569f13319:/src/mc/mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index bee23e103c..0d58509838 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -72,6 +72,7 @@ mc_stats_pair_t mc_stats_pair = NULL;
 xbt_fifo_t mc_stack_liveness = NULL;
 mc_snapshot_t initial_snapshot_liveness = NULL;
 int compare;
+extern xbt_dynar_t mmalloc_ignore;
 
 xbt_automaton_t _mc_property_automaton = NULL;
 
@@ -161,6 +162,11 @@ void MC_modelcheck_liveness(){
   
   mc_time = xbt_new0(double, simix_process_maxpid);
 
+  /* mc_time refers to clock for each process -> ignore it for heap comparison */
+  int i;
+  for(i = 0; i<simix_process_maxpid; i++)
+    MC_ignore(&(mc_time[i]), sizeof(double));
+  
   compare = 0;
 
   /* Initialize the data structures that must be persistent across every
@@ -632,3 +638,19 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
     MC_UNSET_RAW_MEM;
   
 }
+
+void MC_ignore_init(){
+  MC_SET_RAW_MEM;
+  mmalloc_ignore = xbt_dynar_new(sizeof(mc_ignore_region_t), NULL);
+  MC_UNSET_RAW_MEM;
+}
+
+void MC_ignore(void *address, size_t size){
+  MC_SET_RAW_MEM;
+  mc_ignore_region_t region = NULL;
+  region = xbt_new0(s_mc_ignore_region_t, 1);
+  region->address = address;
+  region->size = size;
+  xbt_dynar_push(mmalloc_ignore, &region);
+  MC_UNSET_RAW_MEM;
+}