Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : minor fix
[simgrid.git] / src / mc / mc_compare.c
1 /* Copyright (c) 2012-2013. The SimGrid Team.
2  * All rights reserved.                                                     */
3
4 /* This program is free software; you can redistribute it and/or modify it
5  * under the terms of the license (GNU LGPL) which comes with this package. */
6
7 #include "mc_private.h"
8
9 #include "xbt/mmalloc.h"
10
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc,
12                                 "Logging specific to mc_compare");
13
14 typedef struct s_pointers_pair{
15   void *p1;
16   void *p2;
17 }s_pointers_pair_t, *pointers_pair_t;
18
19 __thread xbt_dynar_t compared_pointers;
20
21 /************************** Free functions ****************************/
22 /********************************************************************/
23
24 static void stack_region_free(stack_region_t s){
25   if(s){
26     xbt_free(s->process_name);
27     xbt_free(s);
28   }
29 }
30
31 static void stack_region_free_voidp(void *s){
32   stack_region_free((stack_region_t) * (void **) s);
33 }
34
35 static void pointers_pair_free(pointers_pair_t p){
36   xbt_free(p);
37 }
38
39 static void pointers_pair_free_voidp(void *p){
40   pointers_pair_free((pointers_pair_t) * (void **)p);
41 }
42
43 /************************** Snapshot comparison *******************************/
44 /******************************************************************************/
45
46 static int already_compared_pointers(void *p1, void *p2){
47
48   if(xbt_dynar_is_empty(compared_pointers))
49     return -1;
50
51   unsigned int cursor = 0;
52   int start = 0;
53   int end = xbt_dynar_length(compared_pointers) - 1;
54   pointers_pair_t pair;
55
56   while(start <= end){
57     cursor = (start + end) / 2;
58     pair = (pointers_pair_t)xbt_dynar_get_as(compared_pointers, cursor, pointers_pair_t);
59     if(pair->p1 == p1){
60       if(pair->p2 == p2)
61         return 0;
62       else if(pair->p2 < p2)
63         start = cursor + 1;
64       else
65         end = cursor - 1;
66     }else if(pair->p1 < p1){
67       start = cursor + 1;
68     }else{
69       end = cursor - 1 ;
70     }
71   }
72
73   return -1;
74
75 }
76
77 static void add_compared_pointers(void *p1, void *p2){
78
79   pointers_pair_t new_pair = xbt_new0(s_pointers_pair_t, 1);
80   new_pair->p1 = p1;
81   new_pair->p2 = p2;
82   
83   if(xbt_dynar_is_empty(compared_pointers)){
84     xbt_dynar_push(compared_pointers, &new_pair);
85     return;
86   }
87
88   unsigned int cursor = 0;
89   int start = 0;
90   int end = xbt_dynar_length(compared_pointers) - 1;
91   pointers_pair_t pair = NULL;
92
93   while(start <= end){
94     cursor = (start + end) / 2;
95     pair = (pointers_pair_t)xbt_dynar_get_as(compared_pointers, cursor, pointers_pair_t);
96     if(pair->p1 == p1){
97       if(pair->p2 == p2){
98         pointers_pair_free(new_pair);
99         return;
100       }else if(pair->p2 < p2)
101         start = cursor + 1;
102       else
103         end = cursor - 1;
104     }else if(pair->p1 < p1){
105       start = cursor + 1;
106     }else{
107       end = cursor - 1 ;
108     }
109   }
110
111   if(pair->p1 == p1){
112     if(pair->p2 < p2)
113       xbt_dynar_insert_at(compared_pointers, cursor + 1, &new_pair);
114     else
115       xbt_dynar_insert_at(compared_pointers, cursor, &new_pair); 
116   }else{
117     if(pair->p1 < p1)
118       xbt_dynar_insert_at(compared_pointers, cursor + 1, &new_pair);
119     else
120       xbt_dynar_insert_at(compared_pointers, cursor, &new_pair);   
121   }
122
123 }
124
125 static int compare_areas_with_type(void *area1, void *area2, xbt_dict_t types, xbt_dict_t other_types, char *type_id, int region_size, int region_type, void *start_data, int pointer_level){
126
127   dw_type_t type = xbt_dict_get_or_null(types, type_id);;
128   unsigned int cursor = 0;
129   dw_type_t member, subtype, subsubtype;
130   int elm_size, i, res, switch_types = 0;
131   void *addr_pointed1, *addr_pointed2;
132
133   switch(type->type){
134   case DW_TAG_base_type:
135   case DW_TAG_enumeration_type:
136   case DW_TAG_union_type:
137     return (memcmp(area1, area2, type->byte_size) != 0);
138     break;
139   case DW_TAG_typedef:
140   case DW_TAG_volatile_type:
141     return compare_areas_with_type(area1, area2, types, other_types, type->dw_type_id, region_size, region_type, start_data, pointer_level);
142     break;
143   case DW_TAG_const_type: /* Const variable cannot be modified */
144     return -1;
145     break;
146   case DW_TAG_array_type:
147     subtype = xbt_dict_get_or_null(types, type->dw_type_id);
148     switch(subtype->type){
149     case DW_TAG_base_type:
150     case DW_TAG_enumeration_type:
151     case DW_TAG_pointer_type:
152     case DW_TAG_structure_type:
153     case DW_TAG_union_type:
154       if(subtype->byte_size == 0){ /*declaration of the type, need the complete description */
155         subtype = xbt_dict_get_or_null(types, get_type_description(types, subtype->name));
156         if(subtype == NULL){
157           subtype = xbt_dict_get_or_null(other_types, get_type_description(other_types, subtype->name));
158           switch_types = 1;
159         }
160       }
161       elm_size = subtype->byte_size;
162       break;
163     case DW_TAG_typedef:
164     case DW_TAG_volatile_type:
165       subsubtype = xbt_dict_get_or_null(types, subtype->dw_type_id);
166       if(subsubtype->byte_size == 0){ /*declaration of the type, need the complete description */
167         subsubtype = xbt_dict_get_or_null(types, get_type_description(types, subsubtype->name));
168         if(subsubtype == NULL){
169           subsubtype = xbt_dict_get_or_null(other_types, get_type_description(other_types, subsubtype->name));
170           switch_types = 1;
171         }
172       }
173       elm_size = subsubtype->byte_size;
174       break;
175     default : 
176       return 0;
177       break;
178     }
179     for(i=0; i<type->element_count; i++){
180       if(switch_types)
181         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);
182       else
183         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);
184       if(res == 1)
185         return res;
186     }
187     break;
188   case DW_TAG_pointer_type:
189     if(type->dw_type_id && ((dw_type_t)xbt_dict_get_or_null(types, type->dw_type_id))->type == DW_TAG_subroutine_type){
190       addr_pointed1 = *((void **)(area1)); 
191       addr_pointed2 = *((void **)(area2));
192       return (addr_pointed1 != addr_pointed2);
193     }else{
194       addr_pointed1 = *((void **)(area1)); 
195       addr_pointed2 = *((void **)(area2));
196       
197       if(addr_pointed1 == NULL && addr_pointed2 == NULL)
198         return 0;
199       if(already_compared_pointers(addr_pointed1, addr_pointed2) != -1)
200         return 0;
201       add_compared_pointers(addr_pointed1, addr_pointed2);
202
203       pointer_level++;
204       
205       if(addr_pointed1 > std_heap && (char *)addr_pointed1 < (char*) std_heap + STD_HEAP_SIZE && addr_pointed2 > std_heap && (char *)addr_pointed2 < (char*) std_heap + STD_HEAP_SIZE){
206         return compare_heap_area(addr_pointed1, addr_pointed2, NULL, types, other_types, type->dw_type_id, pointer_level); 
207       }else if(addr_pointed1 > start_data && (char*)addr_pointed1 <= (char *)start_data + region_size && addr_pointed2 > start_data && (char*)addr_pointed2 <= (char *)start_data + region_size){
208         if(type->dw_type_id == NULL)
209           return  (addr_pointed1 != addr_pointed2);
210         else
211           return  compare_areas_with_type(addr_pointed1, addr_pointed2, types, other_types, type->dw_type_id, region_size, region_type, start_data, pointer_level); 
212       }else{
213         return (addr_pointed1 != addr_pointed2);
214       }
215     }
216     break;
217   case DW_TAG_structure_type:
218     xbt_dynar_foreach(type->members, cursor, member){
219       res = compare_areas_with_type((char *)area1 + member->offset, (char *)area2 + member->offset, types, other_types, member->dw_type_id, region_size, region_type, start_data, pointer_level);
220       if(res == 1)
221         return res;
222     }
223     break;
224   case DW_TAG_subroutine_type:
225     return -1;
226     break;
227   default:
228     XBT_VERB("Unknown case : %d", type->type);
229     break;
230   }
231   
232   return 0;
233 }
234
235 static int compare_global_variables(int region_type, mc_mem_region_t r1, mc_mem_region_t r2){
236
237   if(!compared_pointers){
238     compared_pointers = xbt_dynar_new(sizeof(pointers_pair_t), pointers_pair_free_voidp);
239     MC_ignore_global_variable("compared_pointers");
240   }else{
241     xbt_dynar_reset(compared_pointers);
242   }
243
244   xbt_dynar_t variables;
245   xbt_dict_t types, other_types;
246   int res;
247   unsigned int cursor = 0;
248   dw_variable_t current_var;
249   size_t offset;
250   void *start_data;
251   void* start_data_binary = mc_binary_info->start_data;
252   void* start_data_libsimgrid = mc_libsimgrid_info->start_data;
253
254   mc_object_info_t object_info = NULL;
255   mc_object_info_t other_object_info = NULL;
256   if(region_type == 2){
257     object_info = mc_binary_info;
258     other_object_info = mc_libsimgrid_info;
259     start_data = start_data_binary;
260   }else{
261     object_info = mc_libsimgrid_info;
262     other_object_info = mc_binary_info;
263     start_data = start_data_libsimgrid;
264   }
265   variables = object_info->global_variables;
266   types = object_info->types;
267   other_types = other_object_info->types;
268
269   xbt_dynar_foreach(variables, cursor, current_var){
270
271     if(region_type == 2)
272       offset = (char *)current_var->address.address - (char *)start_data_binary;
273     else
274       offset = (char *)current_var->address.address - (char *)start_data_libsimgrid;
275
276     res = compare_areas_with_type((char *)r1->data + offset, (char *)r2->data + offset, types, other_types, current_var->type_origin, r1->size, region_type, start_data, 0);
277     if(res == 1){
278       XBT_VERB("Global variable %s (%p - %p) is different between snapshots", current_var->name, (char *)r1->data + offset, (char *)r2->data + offset);
279       xbt_dynar_free(&compared_pointers);
280       compared_pointers = NULL;
281       return 1;
282     }
283
284   }
285
286   xbt_dynar_free(&compared_pointers);
287   compared_pointers = NULL;
288
289   return 0;
290
291 }
292
293 static int compare_local_variables(mc_snapshot_stack_t stack1, mc_snapshot_stack_t stack2, void *heap1, void *heap2){
294   void* start_data_binary = mc_binary_info->start_data;
295   void* start_data_libsimgrid = mc_libsimgrid_info->start_data;
296
297   if(!compared_pointers){
298     compared_pointers = xbt_dynar_new(sizeof(pointers_pair_t), pointers_pair_free_voidp);
299     MC_ignore_global_variable("compared_pointers");
300   }else{
301     xbt_dynar_reset(compared_pointers);
302   }
303
304   if(xbt_dynar_length(stack1->local_variables) != xbt_dynar_length(stack2->local_variables)){
305     XBT_VERB("Different number of local variables");
306     xbt_dynar_free(&compared_pointers);
307     compared_pointers = NULL;
308     return 1;
309   }else{
310     unsigned int cursor = 0;
311     local_variable_t current_var1, current_var2;
312     int offset1, offset2, res;
313     while(cursor < xbt_dynar_length(stack1->local_variables)){
314       current_var1 = (local_variable_t)xbt_dynar_get_as(stack1->local_variables, cursor, local_variable_t);
315       current_var2 = (local_variable_t)xbt_dynar_get_as(stack2->local_variables, cursor, local_variable_t);
316       if(strcmp(current_var1->name, current_var2->name) != 0 || strcmp(current_var1->frame, current_var2->frame) != 0 || current_var1->ip != current_var2->ip){
317         xbt_dynar_free(&compared_pointers);
318         XBT_VERB("Different name of variable (%s - %s) or frame (%s - %s) or ip (%lu - %lu)", current_var1->name, current_var2->name, current_var1->frame, current_var2->frame, current_var1->ip, current_var2->ip);
319         return 1;
320       }
321       offset1 = (char *)current_var1->address - (char *)std_heap;
322       offset2 = (char *)current_var2->address - (char *)std_heap;
323       if(current_var1->region == 1)
324         res = compare_areas_with_type( (char *)heap1 + offset1, (char *)heap2 + offset2, mc_libsimgrid_info->types, mc_binary_info->types, current_var1->type, 0, 1, start_data_libsimgrid, 0);
325       else
326         res = compare_areas_with_type( (char *)heap1 + offset1, (char *)heap2 + offset2, mc_binary_info->types, mc_libsimgrid_info->types, current_var1->type, 0, 2, start_data_binary, 0);
327       if(res == 1){
328         XBT_VERB("Local variable %s (%p - %p) in frame %s  is different between snapshots", current_var1->name,(char *)heap1 + offset1, (char *)heap2 + offset2, current_var1->frame);
329         xbt_dynar_free(&compared_pointers);
330         compared_pointers = NULL;
331         return res;
332       }
333       cursor++;
334     }
335     xbt_dynar_free(&compared_pointers);
336     compared_pointers = NULL;
337     return 0;
338   }
339 }
340
341 int snapshot_compare(void *state1, void *state2){
342
343   mc_snapshot_t s1, s2;
344   int num1, num2;
345   
346   if(_sg_mc_property_file && _sg_mc_property_file[0] != '\0'){ /* Liveness MC */
347     s1 = ((mc_visited_pair_t)state1)->graph_state->system_state;
348     s2 = ((mc_visited_pair_t)state2)->graph_state->system_state;
349     num1 = ((mc_visited_pair_t)state1)->num;
350     num2 =  ((mc_visited_pair_t)state2)->num;
351     /* Firstly compare automaton state */
352     /*if(xbt_automaton_state_compare(((mc_pair_t)state1)->automaton_state, ((mc_pair_t)state2)->automaton_state) != 0)
353       return 1;
354     if(xbt_automaton_propositional_symbols_compare_value(((mc_pair_t)state1)->atomic_propositions, ((mc_pair_t)state2)->atomic_propositions) != 0)
355     return 1;*/
356   }else{ /* Safety MC */
357     s1 = ((mc_visited_state_t)state1)->system_state;
358     s2 = ((mc_visited_state_t)state2)->system_state;
359     num1 = ((mc_visited_state_t)state1)->num;
360     num2 = ((mc_visited_state_t)state2)->num;
361   }
362
363   int errors = 0;
364   int res_init;
365
366   xbt_os_timer_t global_timer = xbt_os_timer_new();
367   xbt_os_timer_t timer = xbt_os_timer_new();
368
369   xbt_os_walltimer_start(global_timer);
370
371   #ifdef MC_DEBUG
372     xbt_os_walltimer_start(timer);
373   #endif
374
375   /* Compare size of stacks */
376   int i = 0;
377   size_t size_used1, size_used2;
378   int is_diff = 0;
379   while(i < xbt_dynar_length(s1->stacks)){
380     size_used1 = s1->stack_sizes[i];
381     size_used2 = s2->stack_sizes[i];
382     if(size_used1 != size_used2){
383     #ifdef MC_DEBUG
384       if(is_diff == 0){
385         xbt_os_walltimer_stop(timer);
386         mc_comp_times->stacks_sizes_comparison_time = xbt_os_timer_elapsed(timer);
387       }
388       XBT_DEBUG("(%d - %d) Different size used in stacks : %zu - %zu", num1, num2, size_used1, size_used2);
389       errors++;
390       is_diff = 1;
391     #else
392       #ifdef MC_VERBOSE
393       XBT_VERB("(%d - %d) Different size used in stacks : %zu - %zu", num1, num2, size_used1, size_used2);
394       #endif
395
396       xbt_os_walltimer_stop(timer);
397       xbt_os_timer_free(timer);
398       xbt_os_walltimer_stop(global_timer);
399       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
400       xbt_os_timer_free(global_timer);
401
402       return 1;
403     #endif  
404     }
405     i++;
406   }
407
408   #ifdef MC_DEBUG
409     if(is_diff == 0)
410       xbt_os_walltimer_stop(timer);
411     xbt_os_walltimer_start(timer);
412   #endif
413
414   /* Compare hash of global variables */
415   if(s1->hash_global != NULL && s2->hash_global != NULL){
416     if(strcmp(s1->hash_global, s2->hash_global) != 0){
417       #ifdef MC_DEBUG
418         xbt_os_walltimer_stop(timer);
419         mc_comp_times->hash_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
420         XBT_DEBUG("Different hash of global variables : %s - %s", s1->hash_global, s2->hash_global); 
421         errors++; 
422       #else
423         #ifdef MC_VERBOSE
424           XBT_VERB("Different hash of global variables : %s - %s", s1->hash_global, s2->hash_global); 
425         #endif
426
427         xbt_os_walltimer_stop(timer);
428         xbt_os_timer_free(timer);
429         xbt_os_walltimer_stop(global_timer);
430         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
431         xbt_os_timer_free(global_timer);
432
433         return 1;
434       #endif
435     }
436   }
437
438   #ifdef MC_DEBUG
439     xbt_os_walltimer_start(timer);
440   #endif
441
442   /* Compare hash of local variables */
443   if(s1->hash_local != NULL && s2->hash_local != NULL){
444     if(strcmp(s1->hash_local, s2->hash_local) != 0){
445       #ifdef MC_DEBUG
446         xbt_os_walltimer_stop(timer);
447         mc_comp_times->hash_local_variables_comparison_time = xbt_os_timer_elapsed(timer);
448         XBT_DEBUG("Different hash of local variables : %s - %s", s1->hash_local, s2->hash_local); 
449         errors++; 
450       #else
451         #ifdef MC_VERBOSE
452           XBT_VERB("Different hash of local variables : %s - %s", s1->hash_local, s2->hash_local); 
453         #endif
454
455         xbt_os_walltimer_stop(timer);
456         xbt_os_timer_free(timer);
457         xbt_os_walltimer_stop(global_timer);
458         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
459         xbt_os_timer_free(global_timer);
460
461         return 1;
462       #endif
463     }
464   }
465
466   #ifdef MC_DEBUG
467     xbt_os_walltimer_start(timer);
468   #endif
469
470   /* Init heap information used in heap comparison algorithm */
471   res_init = init_heap_information((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data, s1->to_ignore, s2->to_ignore);
472   if(res_init == -1){
473      #ifdef MC_DEBUG
474     XBT_DEBUG("(%d - %d) Different heap information", num1, num2); 
475         errors++; 
476       #else
477         #ifdef MC_VERBOSE
478         XBT_VERB("(%d - %d) Different heap information", num1, num2); 
479         #endif
480
481         xbt_os_walltimer_stop(global_timer);
482         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
483         xbt_os_timer_free(global_timer);
484
485         return 1;
486       #endif
487   }
488
489   #ifdef MC_DEBUG
490     xbt_os_walltimer_start(timer);
491   #endif
492
493   /* Stacks comparison */
494   unsigned int  cursor = 0;
495   int diff_local = 0;
496   is_diff = 0;
497   mc_snapshot_stack_t stack1, stack2;
498     
499   while(cursor < xbt_dynar_length(s1->stacks)){
500     stack1 = (mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t);
501     stack2 = (mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t);
502     diff_local = compare_local_variables(stack1, stack2, s1->regions[0]->data, s2->regions[0]->data);
503     if(diff_local > 0){
504       #ifdef MC_DEBUG
505         if(is_diff == 0){
506           xbt_os_walltimer_stop(timer);
507           mc_comp_times->stacks_comparison_time = xbt_os_timer_elapsed(timer);
508         }
509         XBT_DEBUG("(%d - %d) Different local variables between stacks %d", num1, num2, cursor + 1);
510         errors++;
511         is_diff = 1;
512       #else
513         
514         #ifdef MC_VERBOSE
515         XBT_VERB("(%d - %d) Different local variables between stacks %d", num1, num2, cursor + 1);
516         #endif
517           
518         reset_heap_information();
519         xbt_os_walltimer_stop(timer);
520         xbt_os_timer_free(timer);
521         xbt_os_walltimer_stop(global_timer);
522         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
523         xbt_os_timer_free(global_timer);
524  
525         return 1;
526       #endif
527     }
528     cursor++;
529   }
530
531   #ifdef MC_DEBUG
532     if(is_diff == 0)
533       xbt_os_walltimer_stop(timer);
534     xbt_os_walltimer_start(timer);
535   #endif
536
537   /* Compare binary global variables */
538   is_diff = compare_global_variables(2, s1->regions[2], s2->regions[2]);
539   if(is_diff != 0){
540     #ifdef MC_DEBUG
541       xbt_os_walltimer_stop(timer);
542       mc_comp_times->binary_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
543       XBT_DEBUG("(%d - %d) Different global variables in binary", num1, num2);
544       errors++;
545     #else
546       #ifdef MC_VERBOSE
547       XBT_VERB("(%d - %d) Different global variables in binary", num1, num2);
548       #endif
549
550       reset_heap_information();
551       xbt_os_walltimer_stop(timer);
552       xbt_os_timer_free(timer);
553       xbt_os_walltimer_stop(global_timer);
554       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
555       xbt_os_timer_free(global_timer);
556
557       return 1;
558     #endif
559   }
560
561   #ifdef MC_DEBUG
562     if(is_diff == 0)
563       xbt_os_walltimer_stop(timer);
564     xbt_os_walltimer_start(timer);
565   #endif
566
567   /* Compare libsimgrid global variables */
568   is_diff = compare_global_variables(1, s1->regions[1], s2->regions[1]);
569   if(is_diff != 0){
570     #ifdef MC_DEBUG
571       xbt_os_walltimer_stop(timer);
572       mc_comp_times->libsimgrid_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
573       XBT_DEBUG("(%d - %d) Different global variables in libsimgrid", num1, num2);
574       errors++;
575     #else
576       #ifdef MC_VERBOSE
577       XBT_VERB("(%d - %d) Different global variables in libsimgrid", num1, num2);
578       #endif
579         
580       reset_heap_information();
581       xbt_os_walltimer_stop(timer);
582       xbt_os_timer_free(timer);
583       xbt_os_walltimer_stop(global_timer);
584       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
585       xbt_os_timer_free(global_timer);
586
587       return 1;
588     #endif
589   }
590
591   #ifdef MC_DEBUG
592     xbt_os_walltimer_start(timer);
593   #endif
594
595   /* Compare heap */
596     if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[0]->data,
597                             (xbt_mheap_t)s2->regions[0]->data,
598                             mc_libsimgrid_info->types,
599                             mc_binary_info->types) > 0){
600
601     #ifdef MC_DEBUG
602       xbt_os_walltimer_stop(timer);
603       mc_comp_times->heap_comparison_time = xbt_os_timer_elapsed(timer); 
604       XBT_DEBUG("(%d - %d) Different heap (mmalloc_compare)", num1, num2);
605       errors++;
606     #else
607  
608       #ifdef MC_VERBOSE
609       XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", num1, num2);
610       #endif
611        
612       reset_heap_information();
613       xbt_os_walltimer_stop(timer);
614       xbt_os_timer_free(timer);
615       xbt_os_walltimer_stop(global_timer);
616       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
617       xbt_os_timer_free(global_timer);
618
619       return 1;
620     #endif
621   }else{
622     #ifdef MC_DEBUG
623       xbt_os_walltimer_stop(timer);
624     #endif
625   }
626
627   reset_heap_information();
628   
629   xbt_os_walltimer_stop(timer);
630   xbt_os_timer_free(timer);
631
632   #ifdef MC_VERBOSE
633     xbt_os_walltimer_stop(global_timer);
634     mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
635   #endif
636
637   xbt_os_timer_free(global_timer);
638
639   #ifdef MC_DEBUG
640     print_comparison_times();
641   #endif
642
643   return errors > 0;
644   
645 }
646
647 /***************************** Statistics *****************************/
648 /*******************************************************************/
649
650 void print_comparison_times(){
651   XBT_DEBUG("*** Comparison times ***");
652   XBT_DEBUG("- Nb processes : %f", mc_comp_times->nb_processes_comparison_time);
653   XBT_DEBUG("- Nb bytes used : %f", mc_comp_times->bytes_used_comparison_time);
654   XBT_DEBUG("- Stacks sizes : %f", mc_comp_times->stacks_sizes_comparison_time);
655   XBT_DEBUG("- Binary global variables : %f", mc_comp_times->binary_global_variables_comparison_time);
656   XBT_DEBUG("- Libsimgrid global variables : %f", mc_comp_times->libsimgrid_global_variables_comparison_time);
657   XBT_DEBUG("- Heap : %f", mc_comp_times->heap_comparison_time);
658   XBT_DEBUG("- Stacks : %f", mc_comp_times->stacks_comparison_time);
659 }
660
661 /**************************** MC snapshot compare simcall **************************/
662 /***********************************************************************************/
663
664 int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall,
665                                    mc_snapshot_t s1, mc_snapshot_t s2){
666   return snapshot_compare(s1, s2);
667 }
668
669 int MC_compare_snapshots(void *s1, void *s2){
670   
671   MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
672   return simcall_mc_compare_snapshots(s1, s2);
673
674 }