X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/a0c5f40f68a69e5fd2c22643c98aed7570191e21..ab23fd586c00bc3e9ea24f1dcd3d52dd0fc60bce:/src/mc/mc_private.h diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 0de5a9e9f0..86431c79a4 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -183,6 +183,8 @@ typedef struct s_memory_map { } s_memory_map_t, *memory_map_t; memory_map_t get_memory_map(void); +void free_memory_map(memory_map_t map); +void get_plt_section(void); /********************************** DPOR for safety **************************************/ @@ -216,47 +218,17 @@ typedef struct s_mc_pair_reached{ xbt_state_t automaton_state; xbt_dynar_t prop_ato; mc_snapshot_t system_state; - //xbt_dict_t rdv_points; }s_mc_pair_reached_t, *mc_pair_reached_t; -typedef struct s_mc_pair_visited{ - xbt_state_t automaton_state; - xbt_dynar_t prop_ato; - mc_snapshot_t system_state; - int search_cycle; -}s_mc_pair_visited_t, *mc_pair_visited_t; - -typedef struct s_mc_pair_visited_hash{ - xbt_state_t automaton_state; - xbt_dynar_t prop_ato; - unsigned int *hash_regions; - int search_cycle; -}s_mc_pair_visited_hash_t, *mc_pair_visited_hash_t; - -typedef struct s_mc_pair_reached_hash{ - xbt_state_t automaton_state; - xbt_dynar_t prop_ato; - unsigned int *hash_regions; -}s_mc_pair_reached_hash_t, *mc_pair_reached_hash_t; - - - int MC_automaton_evaluate_label(xbt_exp_label_t l); mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st); int reached(xbt_state_t st); void set_pair_reached(xbt_state_t st); -int reached_hash(xbt_state_t st); -void set_pair_reached_hash(xbt_state_t st); int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2); void MC_pair_delete(mc_pair_t pair); void MC_exit_liveness(void); mc_state_t MC_state_pair_new(void); -int visited(xbt_state_t st, int search_cycle); -void set_pair_visited(xbt_state_t st, int search_cycle); -int visited_hash(xbt_state_t st, int search_cycle); -void set_pair_visited_hash(xbt_state_t st, int search_cycle); -unsigned int hash_region(char *str, int str_len); /* **** Double-DFS stateless **** */