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'))
+ 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_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));
{
int raw_mem = (mmalloc_get_current_heap() == raw_heap);
- int value, i = 1;
+ int value, i = 1, count = 1;
char *req_str;
smx_simcall_t req = NULL, saved_req = NULL;
xbt_fifo_item_t item, start_item;
mc_state_t state;
+ smx_process_t process = NULL;
XBT_DEBUG("**** Begin Replay ****");
}
}
+ MC_SET_RAW_MEM;
+ xbt_dict_reset(first_enabled_state);
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process)){
+ char *key = bprintf("%lu", process->pid);
+ char *data = bprintf("%d", count);
+ xbt_dict_set(first_enabled_state, key, data, NULL);
+ xbt_free(key);
+ }
+ }
+ MC_UNSET_RAW_MEM;
+
+
/* Traverse the stack from the state at position start and re-execute the transitions */
for (item = start_item;
item != xbt_fifo_get_first_item(stack);
state = (mc_state_t) xbt_fifo_get_item_content(item);
saved_req = MC_state_get_executed_request(state, &value);
+ MC_SET_RAW_MEM;
+ char *key = bprintf("%lu", saved_req->issuer->pid);
+ xbt_dict_remove(first_enabled_state, key);
+ xbt_free(key);
+ MC_UNSET_RAW_MEM;
+
if(saved_req){
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
xbt_free(req_str);
}
}
-
+
SIMIX_simcall_pre(req, value);
MC_wait_for_requests();
+
+ count++;
+
+ MC_SET_RAW_MEM;
+ /* Insert in dict all enabled processes */
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
+ char *key = bprintf("%lu", process->pid);
+ if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
+ char *data = bprintf("%d", count);
+ xbt_dict_set(first_enabled_state, key, data, NULL);
+ }
+ xbt_free(key);
+ }
+ }
+ MC_UNSET_RAW_MEM;
/* Update statistics */
mc_stats->visited_states++;
mc_stats->executed_transitions++;
+
}
+
XBT_DEBUG("**** End Replay ****");
if(raw_mem)
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();
}
}