mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
MC_UNSET_RAW_MEM;
- if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
- MC_SET_RAW_MEM;
- MC_init_dot_output();
- MC_UNSET_RAW_MEM;
- }
-
if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
if (mc_reduce_kind==e_mc_reduce_unset)
mc_reduce_kind=e_mc_reduce_dpor;
MC_ignore_stack("next_context", "smx_ctx_sysv_suspend_serial");
MC_ignore_stack("i", "smx_ctx_sysv_suspend_serial");
+ /* Ignore local variable about time used for tracing */
+ MC_ignore_stack("start_time", "*");
+
MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times));
MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time));
MC_ignore_data_bss(&mc_time, sizeof(mc_time));
/* Create exploration stack */
mc_stack_safety = xbt_fifo_new();
+ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
+ MC_init_dot_output();
+
MC_UNSET_RAW_MEM;
if(_sg_mc_visited > 0){
/* Create the initial state */
initial_state_liveness = xbt_new0(s_mc_global_t, 1);
+ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
+ MC_init_dot_output();
+
MC_UNSET_RAW_MEM;
MC_ddfs_init();
void MC_exit(void)
{
- MC_SET_RAW_MEM;
- if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
- fprintf(dot_output, "}\n");
- fclose(dot_output);
- }
- MC_UNSET_RAW_MEM;
-
xbt_free(mc_time);
MC_memory_exit();
xbt_abort();
XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
}
XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
+ MC_SET_RAW_MEM;
+ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
+ fprintf(dot_output, "}\n");
+ fclose(dot_output);
+ }
+ MC_UNSET_RAW_MEM;
}
void MC_assert(int prop)
XBT_INFO("Counter-example execution trace:");
MC_dump_stack_safety(mc_stack_safety);
MC_print_statistics(mc_stats);
- MC_SET_RAW_MEM;
- if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
- fprintf(dot_output, "}\n");
- fclose(dot_output);
- }
- MC_UNSET_RAW_MEM;
xbt_abort();
}
}
if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
region->fragment = -1;
- ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore = 1;
+ ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore++;
}else{
region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
- ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment] = 1;
+ ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
}
if(mc_heap_comparison_ignore == NULL){