+static void MC_assert_pair(int prop){
+ if (MC_IS_ENABLED && !prop) {
+ XBT_INFO("**************************");
+ XBT_INFO("*** PROPERTY NOT VALID ***");
+ XBT_INFO("**************************");
+ //XBT_INFO("Counter-example execution trace:");
+ MC_show_stack_liveness(mc_stack_liveness);
+ //MC_dump_snapshot_stack(mc_snapshot_stack);
+ MC_print_statistics_pairs(mc_stats_pair);
+ xbt_abort();
+ }
+}
+
+void MC_process_clock_add(smx_process_t process, double amount)
+{
+ mc_time[process->pid] += amount;
+}
+
+double MC_process_clock_get(smx_process_t process)
+{
+ if(mc_time)
+ return mc_time[process->pid];
+ else
+ return 0;
+}
+
+void MC_diff(void){
+
+ mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
+ MC_take_snapshot_liveness(sn);
+
+ int i;
+
+ XBT_INFO("Number of regions : %u", sn->num_reg);
+
+ for(i=0; i<sn->num_reg; i++){
+
+ switch(sn->regions[i]->type){
+ case 0: /* heap */
+ XBT_INFO("Size of heap : %zu", sn->regions[i]->size);
+ break;
+ case 1 : /* libsimgrid */
+ XBT_INFO("Size of libsimgrid : %zu", sn->regions[i]->size);
+ break;
+ case 2 : /* data program */
+ XBT_INFO("Size of data program : %zu", sn->regions[i]->size);
+ break;
+ case 3 : /* stack */
+ XBT_INFO("Size of stack : %zu", sn->regions[i]->size);
+ XBT_INFO("Start addr of stack : %p", sn->regions[i]->start_addr);
+ break;
+ }
+
+ }
+
+}
+
+void MC_automaton_load(const char *file){
+
+ raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ MC_SET_RAW_MEM;
+
+ if (_mc_property_automaton == NULL)
+ _mc_property_automaton = xbt_automaton_new();
+
+ xbt_automaton_load(_mc_property_automaton,file);
+
+ MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+ else
+ MC_UNSET_RAW_MEM;
+
+}
+
+void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
+
+ raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ MC_SET_RAW_MEM;
+
+ if (_mc_property_automaton == NULL)
+ _mc_property_automaton = xbt_automaton_new();
+
+ xbt_new_propositional_symbol(_mc_property_automaton,id,fct);
+
+ MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+ else
+ MC_UNSET_RAW_MEM;
+
+}