model-checker : ignore irrelevant differences for heap comparison algorithm

[simgrid.git] / src / mc / mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 476c4d4..0d58509 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -71,6 +71,8 @@ mc_stats_t mc_stats = NULL;
 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;
 
@@ -131,6 +133,7 @@ void MC_init_safety(void)
   MC_take_snapshot(initial_snapshot);
   MC_UNSET_RAW_MEM;
 
+
   if(raw_mem_set)
     MC_SET_RAW_MEM;
   else
@@ -138,6 +141,10 @@ void MC_init_safety(void)
   
 }
 
+void MC_compare(void){
+  compare = 1;
+}
+
 
 void MC_modelcheck(void)
 {
@@ -155,6 +162,13 @@ 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
      iteration of the model-checker (in RAW memory) */
 
@@ -585,38 +599,6 @@ double MC_process_clock_get(smx_process_t process)
     return 0;
 }
 
-void MC_diff(void){
-
-  mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_liveness(sn);
-
-  int i;
-
-  XBT_INFO("Number of regions : %u", sn->num_reg);
-
-  for(i=0; i<sn->num_reg; i++){
-    
-    switch(sn->regions[i]->type){
-    case 0: /* heap */
-      XBT_INFO("Size of heap : %zu", sn->regions[i]->size);
-      mmalloc_display_info_heap(sn->regions[i]->data);
-      break;
-    case 1 : /* libsimgrid */
-      XBT_INFO("Size of libsimgrid : %zu", sn->regions[i]->size);
-      break;
-    case 2 : /* data program */
-      XBT_INFO("Size of data program : %zu", sn->regions[i]->size);
-      break;
-    case 3 : /* stack */
-      XBT_INFO("Size of stack : %zu", sn->regions[i]->size);
-      XBT_INFO("Start addr of stack : %p", sn->regions[i]->start_addr);
-      break;
-    }
-
-  }
-
-}
-
 void MC_automaton_load(const char *file){
 
   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@ -656,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;
+}