void MC_assert(int prop)
{
if (MC_is_active() && !prop) {
- XBT_INFO("**************************");
- XBT_INFO("*** PROPERTY NOT VALID ***");
- XBT_INFO("**************************");
- XBT_INFO("Counter-example execution trace:");
- MC_record_dump_path(mc_stack);
- MC_dump_stack_safety(mc_stack);
- MC_print_statistics(mc_stats);
- xbt_abort();
+ if (mc_mode == MC_MODE_STANDALONE) {
+ MC_report_assertion_error();
+ } else {
+ MC_client_send_simple_message(MC_MESSAGE_ASSERTION_FAILED);
+ MC_client_handle_messages();
+ }
}
}
}
// TODO, remove this once the migration has been completed
- int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
MC_process_ignore_memory(&mc_model_checker->process, addr, size);
- if (!raw_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(heap);
}