- // Try to enable core dumps
- struct rlimit core_limit;
- core_limit.rlim_cur = RLIM_INFINITY;
- core_limit.rlim_max = RLIM_INFINITY;
-
- if(setrlimit(RLIMIT_CORE, &core_limit) < 0)
- fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno));
-
- int status;
- switch(fork()){
- case 0:
- // We are the child process -- run the actual program
- abort();
- break;
-
- case -1:
- // An error occurred, shouldn't happen
- perror("fork");
- return -1;
-
- default:
- // We are the parent process -- wait for the child process to exit
- if(wait(&status) < 0)
- perror("wait");
- if(WIFSIGNALED(status) && WCOREDUMP(status)){
- char *core_name = malloc(20);
- sprintf(core_name,"core_%d", pair);
- rename("core", core_name);
- free(core_name);
- }
- }
-
- return 0;
-}
-
-int reached(xbt_state_t st){
-
- raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
- if(xbt_dynar_is_empty(reached_pairs) || !compare){
-
- return 0;
-
- }else{
-
- MC_SET_RAW_MEM;
-
- mc_pair_reached_t new_pair = NULL;
- new_pair = xbt_new0(s_mc_pair_reached_t, 1);
- new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
- new_pair->automaton_state = st;
- new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
- new_pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
- MC_take_snapshot_liveness(new_pair->system_state);
-
- /* Get values of propositional symbols */
- int res;
- int_f_void_t f;
- unsigned int cursor = 0;
- xbt_propositional_symbol_t ps = NULL;
- xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
- f = (int_f_void_t)ps->function;
- res = (*f)();
- xbt_dynar_push_as(new_pair->prop_ato, int, res);
- }
-
- cursor = 0;
- mc_pair_reached_t pair_test = NULL;
-
- xbt_dynar_foreach(reached_pairs, cursor, pair_test){
- XBT_INFO("Pair reached #%d", pair_test->nb);
- if(automaton_state_compare(pair_test->automaton_state, st) == 0){
- if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
- if(snapshot_compare(pair_test->system_state, new_pair->system_state) == 0){
-
- if(raw_mem_set)
- MC_SET_RAW_MEM;
- else
- MC_UNSET_RAW_MEM;
-
- return 1;
- }
- }else{
- XBT_INFO("Different values of propositional symbols");
- }
- }else{
- XBT_INFO("Different automaton state");
- }
- }
-
- /* New pair reached */
- xbt_dynar_push(reached_pairs, &new_pair);
-
- create_dump(xbt_dynar_length(reached_pairs));
-
- MC_UNSET_RAW_MEM;
-
- if(raw_mem_set)
- MC_SET_RAW_MEM;
- else
- MC_UNSET_RAW_MEM;
-
- compare = 0;
-
- return 0;
-
- }
-}
-
-
-void set_pair_reached(xbt_state_t st){
-
- raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
- MC_SET_RAW_MEM;
-
- mc_pair_reached_t pair = NULL;
- pair = xbt_new0(s_mc_pair_reached_t, 1);
- pair->nb = xbt_dynar_length(reached_pairs) + 1;
- pair->automaton_state = st;
- pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
- pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
- MC_take_snapshot_liveness(pair->system_state);
-
- /* Get values of propositional symbols */
- unsigned int cursor = 0;
- xbt_propositional_symbol_t ps = NULL;