X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/5e80b119f85e258080482cb688a6b89e01d74595..2856679722f2a932bcdd28f50776353829a61576:/src/mc/mc_private.h diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index af91f56019..05d2a744ca 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -42,11 +42,15 @@ typedef struct s_mc_snapshot_stack{ void *stack_pointer; }s_mc_snapshot_stack_t, *mc_snapshot_stack_t; +typedef struct s_mc_global_t{ + mc_snapshot_t initial_snapshot; +}s_mc_global_t, *mc_global_t; + void MC_take_snapshot(mc_snapshot_t); -void MC_take_snapshot_liveness(mc_snapshot_t s); +mc_snapshot_t MC_take_snapshot_liveness(void); void MC_restore_snapshot(mc_snapshot_t); void MC_free_snapshot(mc_snapshot_t); - +void snapshot_stack_free_voidp(void *s); /********************************* MC Global **********************************/ extern double *mc_time; @@ -213,13 +217,15 @@ void MC_init_safety(void); /********************************** Double-DFS for liveness property**************************************/ extern xbt_fifo_t mc_stack_liveness; -extern mc_snapshot_t initial_snapshot_liveness; +extern mc_global_t initial_state_liveness; extern xbt_automaton_t _mc_property_automaton; extern int compare; extern void *start_plt_libsimgrid; extern void *end_plt_libsimgrid; extern void *start_plt_binary; extern void *end_plt_binary; +extern xbt_dynar_t mc_stack_comparison_ignore; +extern void *start_bss_libsimgrid; typedef struct s_mc_pair{ mc_snapshot_t system_state; @@ -243,6 +249,10 @@ 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); +void pair_reached_free(mc_pair_reached_t pair); +void pair_reached_free_voidp(void *p); +void MC_init_liveness(void); +void MC_init_memory_map_info(void); /* **** Double-DFS stateless **** */ @@ -257,13 +267,15 @@ 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 MC_pair_stateless_delete(mc_pair_stateless_t pair); +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; extern int _surf_mc_checkpoint; extern char* _surf_mc_property_file; +extern int _surf_mc_timeout; /****** Core dump ******/