int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
+ raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ MC_SET_RAW_MEM;
+
int errors = 0, i;
xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
return 1;
}
if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
return 1;
}
if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[i]->data, (xbt_mheap_t)s2->regions[i]->data, &stacks1, &stacks2, &equals)){
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
return 1;
}
heap1 = s1->regions[i]->data;
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
return 1;
}
if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
return 1;
}
if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
return 1;
}
break;
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
return 1;
}
if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
return 1;
}
if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
return 1;
}
break;
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
return 1;
}else{
XBT_INFO("Local variables are equals in stack %d", cursor + 1);
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
return 0;
}
new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
new_pair->automaton_state = st;
new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
- new_pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
- MC_take_snapshot_liveness(new_pair->system_state);
+ new_pair->system_state = MC_take_snapshot_liveness();
/* Get values of propositional symbols */
int res;
pair->nb = xbt_dynar_length(reached_pairs) + 1;
pair->automaton_state = st;
pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
- pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
- MC_take_snapshot_liveness(pair->system_state);
+ pair->system_state = MC_take_snapshot_liveness();
/* Get values of propositional symbols */
unsigned int cursor = 0;
successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
/* Save the initial state */
- initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
- MC_take_snapshot_liveness(initial_snapshot_liveness);
+ initial_snapshot_liveness = MC_take_snapshot_liveness();
MC_UNSET_RAW_MEM;
-
- /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */
- get_libsimgrid_plt_section();
- get_binary_plt_section();
-
+
unsigned int cursor = 0;
xbt_state_t state;
}s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
void MC_take_snapshot(mc_snapshot_t);
-void MC_take_snapshot_liveness(mc_snapshot_t s);
+mc_snapshot_t MC_take_snapshot_liveness(void);
void MC_restore_snapshot(mc_snapshot_t);
void MC_free_snapshot(mc_snapshot_t);
void snapshot_stack_free_voidp(void *s);