model-checker : fix compilation error (with optimizations) with commit d90a41491cfb04...

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

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 0447fa4..ae9f437 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -178,6 +178,16 @@ void MC_init(){
   get_libsimgrid_plt_section();
   get_binary_plt_section();
 
+   /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
+  MC_ignore_stack("e", "*");
+  MC_ignore_stack("__ex_cleanup", "*");
+  MC_ignore_stack("__ex_mctx_en", "*");
+  MC_ignore_stack("__ex_mctx_me", "*");
+  MC_ignore_stack("_log_ev", "*");
+  MC_ignore_stack("_throw_ctx", "*");
+  MC_ignore_stack("ctx", "*");
+
+
   if(raw_mem_set)
     MC_SET_RAW_MEM;
 
@@ -207,7 +217,13 @@ void MC_modelcheck_safety(void)
 
   MC_UNSET_RAW_MEM;
 
-  MC_init();
+  if(_surf_mc_stateful > 0){
+    MC_init();
+  }else{
+    MC_init_memory_map_info();
+    get_libsimgrid_plt_section();
+    get_binary_plt_section();
+  }
 
   MC_dpor_init();
 
@@ -789,7 +805,7 @@ void MC_ignore_data_bss(void *address, size_t size){
     var->address = address;
     var->size = size;
 
-    if(current_var->address > address)
+    if(current_var->address < address)
       xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
     else
       xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var);