Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : sort ignore list and dichotomic search
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Wed, 1 Aug 2012 20:42:47 +0000 (22:42 +0200)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Wed, 1 Aug 2012 20:42:47 +0000 (22:42 +0200)
src/mc/mc_global.c
src/xbt/mmalloc/mm_diff.c

index 0d58509..d91af14 100644 (file)
@@ -646,11 +646,22 @@ void MC_ignore_init(){
 }
 
 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);
+
+  unsigned int cursor = 0;
+  mc_ignore_region_t current_region;
+  xbt_dynar_foreach(mmalloc_ignore, cursor, current_region){
+    if(current_region->address > address)
+      break;
+  }
+
+  xbt_dynar_insert_at(mmalloc_ignore, cursor, &region);
+
   MC_UNSET_RAW_MEM;
 }
index 1399808..8098a95 100644 (file)
@@ -356,11 +356,21 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
 static size_t heap_comparison_ignore(void *address){
   unsigned int cursor = 0;
+  int start = 0;
+  int end = xbt_dynar_length(mmalloc_ignore) - 1;
   mc_ignore_region_t region;
-  xbt_dynar_foreach(mmalloc_ignore, cursor, region){
+
+  while(start <= end){
+    cursor = (start + end) / 2;
+    region = (mc_ignore_region_t)xbt_dynar_get_as(mmalloc_ignore, cursor, mc_ignore_region_t);
     if(region->address == address)
       return region->size;
+    if(region->address < address)
+      start = cursor + 1;
+    if(region->address > address)
+      end = cursor - 1;   
   }
+
   return 0;
 }