#include "mc_client.h"
#include "mc_replay.h"
#include "mc_safety.h"
+#include "mc_exit.h"
extern "C" {
static void MC_pre_modelcheck_liveness(void)
{
- initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
mc_pair_t initial_pair = NULL;
smx_process_t process;
XBT_INFO("| ACCEPTANCE CYCLE |");
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
XBT_INFO("Counter-example that violates formula :");
+ MC_record_dump_path(mc_stack);
MC_show_stack_liveness(mc_stack);
MC_dump_stack_liveness(mc_stack);
MC_print_statistics(mc_stats);
XBT_INFO("Counter-example depth : %d", counter_example_depth);
- xbt_abort();
+ exit(SIMGRID_EXIT_LIVENESS);
}
}
MC_pre_modelcheck_liveness();
/* We're done */
+ XBT_INFO("No property violation found.");
MC_print_statistics(mc_stats);
xbt_free(mc_time);
}