Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : update system state comparison
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Sun, 29 Sep 2013 08:17:16 +0000 (10:17 +0200)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Sun, 29 Sep 2013 08:20:52 +0000 (10:20 +0200)
src/mc/mc_compare.c
src/xbt/mmalloc/mm_diff.c

index 096aba5..3cb30bf 100644 (file)
@@ -181,7 +181,7 @@ static int compare_areas_with_type(void *area1, void *area2, xbt_dict_t types, x
         res = compare_areas_with_type((char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), other_types, types, type->dw_type_id, region_size, region_type, start_data, pointer_level);
       else
         res = compare_areas_with_type((char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), types, other_types, type->dw_type_id, region_size, region_type, start_data, pointer_level);
         res = compare_areas_with_type((char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), other_types, types, type->dw_type_id, region_size, region_type, start_data, pointer_level);
       else
         res = compare_areas_with_type((char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), types, other_types, type->dw_type_id, region_size, region_type, start_data, pointer_level);
-      if(res != 0)
+      if(res == 1)
         return res;
     }
     break;
         return res;
     }
     break;
@@ -208,9 +208,9 @@ static int compare_areas_with_type(void *area1, void *area2, xbt_dict_t types, x
         if(type->dw_type_id == NULL)
           return  (addr_pointed1 != addr_pointed2);
         else
         if(type->dw_type_id == NULL)
           return  (addr_pointed1 != addr_pointed2);
         else
-          return compare_areas_with_type(addr_pointed1, addr_pointed2, types, other_types, type->dw_type_id, region_size, region_type, start_data, pointer_level); 
+          return  compare_areas_with_type(addr_pointed1, addr_pointed2, types, other_types, type->dw_type_id, region_size, region_type, start_data, pointer_level); 
       }else{
       }else{
-        return  (addr_pointed1 != addr_pointed2);
+        return (addr_pointed1 != addr_pointed2);
       }
     }
     break;
       }
     }
     break;
index e0141b5..7618035 100644 (file)
@@ -751,7 +751,10 @@ static int compare_heap_area_with_type(void *real_area1, void *real_area2, void
     if((check_ignore > 0) && ((ignore1 = heap_comparison_ignore_size(to_ignore1, real_area1)) > 0) && ((ignore2 = heap_comparison_ignore_size(to_ignore2, real_area2))  == ignore1))
       return 0;
     if(strcmp(type->name, "char") == 0){ /* String, hence random (arbitrary ?) size */
     if((check_ignore > 0) && ((ignore1 = heap_comparison_ignore_size(to_ignore1, real_area1)) > 0) && ((ignore2 = heap_comparison_ignore_size(to_ignore2, real_area2))  == ignore1))
       return 0;
     if(strcmp(type->name, "char") == 0){ /* String, hence random (arbitrary ?) size */
-      return (memcmp(area1, area2, area_size) != 0);
+      if(real_area1 == real_area2)
+        return -1;
+      else
+        return (memcmp(area1, area2, area_size) != 0);
     }else{
       if(area_size != -1 && type->size != area_size)
         return -1;
     }else{
       if(area_size != -1 && type->size != area_size)
         return -1;
@@ -885,7 +888,8 @@ static int compare_heap_area_with_type(void *real_area1, void *real_area2, void
   case e_dw_union_type:
     if((check_ignore > 0) && ((ignore1 = heap_comparison_ignore_size(to_ignore1, real_area1)) > 0) && ((ignore2 = heap_comparison_ignore_size(to_ignore2, real_area2))  == ignore1))
       return 0;
   case e_dw_union_type:
     if((check_ignore > 0) && ((ignore1 = heap_comparison_ignore_size(to_ignore1, real_area1)) > 0) && ((ignore2 = heap_comparison_ignore_size(to_ignore2, real_area2))  == ignore1))
       return 0;
-    return compare_heap_area_without_type(real_area1, real_area2, area1, area2, previous, all_types, other_types, type->size, check_ignore);
+    else
+      return compare_heap_area_without_type(real_area1, real_area2, area1, area2, previous, all_types, other_types, type->size, check_ignore);
     break;
   case e_dw_volatile_type:
     return compare_heap_area_with_type(real_area1, real_area2, area1, area2, previous, all_types, other_types, type->dw_type_id, area_size, check_ignore, pointer_level);
     break;
   case e_dw_volatile_type:
     return compare_heap_area_with_type(real_area1, real_area2, area1, area2, previous, all_types, other_types, type->dw_type_id, area_size, check_ignore, pointer_level);
@@ -909,6 +913,7 @@ int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t
   void *area1_to_compare, *area2_to_compare;
   dw_type_t type = NULL;
   char *type_desc;
   void *area1_to_compare, *area2_to_compare;
   dw_type_t type = NULL;
   char *type_desc;
+  int type_size = -1;
 
   int match_pairs = 0;
 
 
   int match_pairs = 0;
 
@@ -938,6 +943,25 @@ int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t
 
   addr_block1 = ((void*) (((ADDR2UINT(block1)) - 1) * BLOCKSIZE + (char*)heapbase1));
   addr_block2 = ((void*) (((ADDR2UINT(block2)) - 1) * BLOCKSIZE + (char*)heapbase2));
 
   addr_block1 = ((void*) (((ADDR2UINT(block1)) - 1) * BLOCKSIZE + (char*)heapbase1));
   addr_block2 = ((void*) (((ADDR2UINT(block2)) - 1) * BLOCKSIZE + (char*)heapbase2));
+
+  if(type_id){
+    type = xbt_dict_get_or_null(all_types, type_id);
+    if(type->size == 0){
+      if(type->dw_type_id == NULL){
+        type_desc = get_type_description(all_types, type->name);
+        if(type_desc)
+          type = xbt_dict_get_or_null(all_types, type_desc);
+        else
+          type = xbt_dict_get_or_null(other_types, get_type_description(other_types, type->name));
+      }else{
+        type = xbt_dict_get_or_null(all_types, type->dw_type_id);
+      }
+    }
+    if((type->type == e_dw_pointer_type) || ((type->type == e_dw_base_type) && (!strcmp(type->name, "char"))))
+      type_size = -1;
+    else
+      type_size = type->size;
+  }
   
   if((heapinfo1[block1].type == -1) && (heapinfo2[block2].type == -1)){  /* Free block */
 
   
   if((heapinfo1[block1].type == -1) && (heapinfo2[block2].type == -1)){  /* Free block */
 
@@ -959,25 +983,9 @@ int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t
       }
     }
 
       }
     }
 
-    if(type_id){
-      type = xbt_dict_get_or_null(all_types, type_id);
-      if(strcmp(type->name, "char") ==0){
-        if(area1 == area2)
-          return -1;
-      }
-      if(type->size == 0){
-        type_desc = get_type_description(all_types, type->name);
-        if(type_desc)
-          type = xbt_dict_get_or_null(all_types, type_desc);
-        else
-          type = xbt_dict_get_or_null(other_types, get_type_description(other_types, type->name));
-      }
-      if(strcmp(type->name, "s_smx_context") != 0){
-        if(type->size > 0){
-          if(heapinfo1[block1].busy_block.busy_size != type->size && heapinfo2[block2].busy_block.busy_size  != type->size)
-            return -1;
-        }
-      }
+    if(type_size != -1){
+      if(type_size != heapinfo1[block1].busy_block.busy_size && type_size != heapinfo2[block2].busy_block.busy_size && strcmp(type->name, "s_smx_context") != 0)
+        return -1;
     }
 
     if(heapinfo1[block1].busy_block.size != heapinfo2[block2].busy_block.size){
     }
 
     if(heapinfo1[block1].busy_block.size != heapinfo2[block2].busy_block.size){
@@ -1032,27 +1040,11 @@ int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t
     area1_to_compare = addr_frag1;
     area2_to_compare = addr_frag2;
 
     area1_to_compare = addr_frag1;
     area2_to_compare = addr_frag2;
 
-    if(type_id){
-      type = xbt_dict_get_or_null(all_types, type_id);
-      if(strcmp(type->name, "char") ==0){
-        if(area1 == area2)
-          return -1;
-      }
-      if(type->size == 0 || type->type == e_dw_pointer_type){
-        if(!type->dw_type_id){
-          type_desc = get_type_description(all_types, type->name);
-          if(type_desc)
-            type = xbt_dict_get_or_null(all_types, type_desc);
-          else
-            type = xbt_dict_get_or_null(other_types, get_type_description(other_types, type->name));
-        }else{
-          type = xbt_dict_get_or_null(all_types, type->dw_type_id);
-        }
-      }
-      if(type->size > 0){
-        if(heapinfo1[block1].busy_frag.frag_size[frag1] != type->size || heapinfo2[block2].busy_frag.frag_size[frag2]  != type->size)
-          return -1;
-      }
+    if(type_size != -1){
+      if(heapinfo1[block1].busy_frag.frag_size[frag1] == -1 || heapinfo2[block2].busy_frag.frag_size[frag2] == -1)
+        return -1;
+      if(type_size != heapinfo1[block1].busy_frag.frag_size[frag1] && type_size !=  heapinfo2[block2].busy_frag.frag_size[frag2])
+        return -1;
     }
 
     if(equals_to1[block1][frag1] != NULL && equals_to2[block2][frag2] != NULL){
     }
 
     if(equals_to1[block1][frag1] != NULL && equals_to2[block2][frag2] != NULL){
@@ -1066,10 +1058,14 @@ int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t
     }
 
     if(heapinfo1[block1].busy_frag.frag_size[frag1] != heapinfo2[block2].busy_frag.frag_size[frag2]){
     }
 
     if(heapinfo1[block1].busy_frag.frag_size[frag1] != heapinfo2[block2].busy_frag.frag_size[frag2]){
-      if(match_pairs){
-        xbt_dynar_free(&previous);
+      if(type_size == -1){
+        return -1;
+      }else{
+        if(match_pairs){
+          xbt_dynar_free(&previous);
+        }
+        return 1;
       }
       }
-      return 1;
     }
       
     if(!add_heap_area_pair(previous, block1, frag1, block2, frag2)){
     }
       
     if(!add_heap_area_pair(previous, block1, frag1, block2, frag2)){