X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/28700bafbbef119ee34d7632ed7c61749995dc78..e7c0c67af63b3979a597a66e5e1c8b0435fc6e19:/src/include/mc/mc.h?ds=sidebyside diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 7b3cb1d67e..65c8212973 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -27,11 +27,12 @@ extern char* _sg_mc_property_file; extern int _sg_mc_timeout; extern int _sg_mc_max_depth; extern int _sg_mc_visited; - -extern char*_surf_mc_property_file; /* fixme: better location? */ +extern char* _sg_mc_dot_output_file; extern xbt_dynar_t mc_heap_comparison_ignore; extern xbt_dynar_t stacks_areas; +extern void *maestro_stack_start; +extern void *maestro_stack_end; /********************************* Global *************************************/ void _mc_cfg_cb_reduce(const char *name, int pos); @@ -40,12 +41,12 @@ void _mc_cfg_cb_property(const char *name, int pos); void _mc_cfg_cb_timeout(const char *name, int pos); void _mc_cfg_cb_max_depth(const char *name, int pos); void _mc_cfg_cb_visited(const char *name, int pos); +void _mc_cfg_cb_dot_output(const char *name, int pos); XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void); XBT_PUBLIC(void) MC_init(void); XBT_PUBLIC(void) MC_exit(void); -XBT_PUBLIC(void) MC_exit_liveness(void); XBT_PUBLIC(void) MC_modelcheck_safety(void); XBT_PUBLIC(void) MC_modelcheck_liveness(void); XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double); @@ -54,6 +55,7 @@ void MC_automaton_load(const char *file); /****************************** MC ignore **********************************/ XBT_PUBLIC(void) MC_ignore_heap(void *address, size_t size); +XBT_PUBLIC(void) MC_remove_ignore_heap(void *address, size_t size); XBT_PUBLIC(void) MC_ignore_stack(const char *var_name, const char *frame); XBT_PUBLIC(void) MC_ignore_data_bss(void *address, size_t size); void MC_new_stack_area(void *stack, char *name, void *context, size_t size);