-//#define MC_VERBOSE 1
-
-/********************************** DPOR for safety **************************************/
-typedef enum {
- e_mc_reduce_unset,
- e_mc_reduce_none,
- e_mc_reduce_dpor
-} e_mc_reduce_t;
-
-extern e_mc_reduce_t mc_reduce_kind;
-extern mc_global_t initial_state_safety;
-
-void MC_dpor_init(void);
-void MC_dpor(void);
-void MC_init(void);
-
-typedef struct s_mc_safety_visited_state{
- mc_snapshot_t system_state;
- int num;
-}s_mc_safety_visited_state_t, *mc_safety_visited_state_t;
-
-
-/********************************** Double-DFS for liveness property**************************************/
-
-extern xbt_fifo_t mc_stack_liveness;
-extern mc_global_t initial_state_liveness;
-extern xbt_automaton_t _mc_property_automaton;
-extern int compare;
-extern xbt_dynar_t mc_stack_comparison_ignore;
-extern xbt_dynar_t mc_data_bss_comparison_ignore;
-
-
-typedef struct s_mc_pair{
- mc_snapshot_t system_state;
- mc_state_t graph_state;
- xbt_state_t automaton_state;
-}s_mc_pair_t, *mc_pair_t;
-
-typedef struct s_mc_pair_reached{
- int nb;
- xbt_state_t automaton_state;
- xbt_dynar_t prop_ato;
- mc_snapshot_t system_state;
-}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;
-}s_mc_pair_visited_t, *mc_pair_visited_t;
-
-int MC_automaton_evaluate_label(xbt_exp_label_t l);
-
-int reached(xbt_state_t st);
-void set_pair_reached(xbt_state_t st);
-int visited(xbt_state_t st);
-
-void MC_pair_delete(mc_pair_t pair);
-mc_state_t MC_state_pair_new(void);
-void pair_reached_free(mc_pair_reached_t pair);
-void pair_reached_free_voidp(void *p);
-void pair_visited_free(mc_pair_visited_t pair);
-void pair_visited_free_voidp(void *p);
-void MC_init_memory_map_info(void);
-
-int get_heap_region_index(mc_snapshot_t s);
-
-/* **** Double-DFS stateless **** */
-
-typedef struct s_mc_pair_stateless{
- mc_state_t graph_state;
- xbt_state_t automaton_state;
- int requests;
-}s_mc_pair_stateless_t, *mc_pair_stateless_t;
-
-mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r);
-void MC_ddfs_init(void);
-void MC_ddfs(int search_cycle);
-void MC_show_stack_liveness(xbt_fifo_t stack);
-void MC_dump_stack_liveness(xbt_fifo_t stack);
-void pair_stateless_free(mc_pair_stateless_t pair);
-void pair_stateless_free_voidp(void *p);
-
-/********************************** Configuration of MC **************************************/
-extern xbt_fifo_t mc_stack_safety;
-
-/****** Core dump ******/
-
-int create_dump(int pair);
-
-/****** Local variables with DWARF ******/
-
-typedef enum {
- e_dw_loclist,
- e_dw_register,
- e_dw_bregister_op,
- e_dw_lit,
- e_dw_fbregister_op,
- e_dw_piece,
- e_dw_arithmetic,
- e_dw_plus_uconst,
- e_dw_compose,
- e_dw_deref,
- e_dw_uconstant,
- e_dw_sconstant,
- e_dw_unsupported
-} e_dw_location_type;
-
-typedef struct s_dw_location{
- e_dw_location_type type;
- union{
-
- xbt_dynar_t loclist;
-
- int reg;
-
- struct{
- unsigned int reg;
- int offset;
- }breg_op;
-
- unsigned int lit;
-
- int fbreg_op;
-
- int piece;
-
- unsigned short int deref_size;
-
- xbt_dynar_t compose;
-
- char *arithmetic;
-
- struct{
- int bytes;
- long unsigned int value;
- }uconstant;
-
- struct{
- int bytes;
- long signed int value;
- }sconstant;
-
- unsigned int plus_uconst;
-
- }location;
-}s_dw_location_t, *dw_location_t;
-
-typedef struct s_dw_location_entry{
- long lowpc;
- long highpc;
- dw_location_t location;
-}s_dw_location_entry_t, *dw_location_entry_t;
-
-typedef struct s_dw_local_variable{
- char *name;
- dw_location_t location;
-}s_dw_local_variable_t, *dw_local_variable_t;