model-checker : cosmectics

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 25de83a..8289f35 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -237,11 +237,11 @@ void MC_modelcheck_safety(void)
   initial_state_safety->snapshot = MC_take_snapshot();
   MC_UNSET_RAW_MEM;
 
   initial_state_safety->snapshot = MC_take_snapshot();
   MC_UNSET_RAW_MEM;
 

+  MC_dpor();
+

   if(raw_mem_set)
     MC_SET_RAW_MEM;
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
 

-  MC_dpor();
-

   MC_exit();
 }
 
   MC_exit();
 }
 


@@ -820,6 +820,32 @@ void MC_ignore_data_bss(void *address, size_t size){
     MC_SET_RAW_MEM;
 }
 
     MC_SET_RAW_MEM;
 }
 

+static size_t data_bss_ignore_size(void *address){
+  unsigned int cursor = 0;
+  int start = 0;
+  int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
+  mc_data_bss_ignore_variable_t var;
+
+  while(start <= end){
+    cursor = (start + end) / 2;
+    var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
+    if(var->address == address)
+      return var->size;
+    if(var->address < address){
+      if((void *)((char *)var->address + var->size) > address)
+        return (char *)var->address + var->size - (char*)address;
+      else
+        start = cursor + 1;
+    }
+    if(var->address > address)
+      end = cursor - 1;   
+  }
+
+  return 0;
+}
+
+
+

 void MC_ignore_stack(const char *var_name, const char *frame){
   
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 void MC_ignore_stack(const char *var_name, const char *frame){
   
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);


@@ -1647,31 +1673,6 @@ void print_local_variables(xbt_dict_t list){
 
 }
 
 
 }
 

-static size_t data_bss_ignore_size(void *address){
-  unsigned int cursor = 0;
-  int start = 0;
-  int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
-  mc_data_bss_ignore_variable_t var;
-
-  while(start <= end){
-    cursor = (start + end) / 2;
-    var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
-    if(var->address == address)
-      return var->size;
-    if(var->address < address){
-      if((void *)((char *)var->address + var->size) > address)
-        return (char *)var->address + var->size - (char*)address;
-      else
-        start = cursor + 1;
-    }
-    if(var->address > address)
-      end = cursor - 1;   
-  }
-
-  return 0;
-}
-
-

 static void MC_get_global_variables(char *elf_file){
 
   FILE *fp;
 static void MC_get_global_variables(char *elf_file){
 
   FILE *fp;