X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/fa222c38f9b796be07ab4351ffc810a61a8fd705..7d87bd675e40074957819b602f38fb905209990e:/src/include/mc/mc.h diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 2f4ec260ca..d3eadeabe2 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -7,6 +7,9 @@ #ifndef _MC_MC_H #define _MC_MC_H +#include + +#include "xbt/base.h" #include "xbt/misc.h" #include "xbt/fifo.h" #include "xbt/dict.h" @@ -35,55 +38,58 @@ SG_BEGIN_DECL() -/********************************** Configuration of MC **************************************/ -extern int _sg_do_model_check; -extern int _sg_do_model_check_record; -extern int _sg_mc_checkpoint; -extern int _sg_mc_sparse_checkpoint; -extern char* _sg_mc_property_file; -extern int _sg_mc_timeout; -extern int _sg_mc_hash; -extern int _sg_mc_max_depth; -extern int _sg_mc_visited; -extern char* _sg_mc_dot_output_file; -extern int _sg_mc_comms_determinism; -extern int _sg_mc_send_determinism; -extern int _sg_mc_safety; -extern int _sg_mc_liveness; -extern int _sg_mc_snapshot_fds; -extern int _sg_mc_termination; - -extern xbt_dynar_t mc_heap_comparison_ignore; -extern xbt_dynar_t stacks_areas; +/********************************** Configuration of MC **************************************/ + +extern XBT_PUBLIC(int) _sg_do_model_check; +extern XBT_PRIVATE int _sg_do_model_check_record; +extern XBT_PRIVATE int _sg_mc_checkpoint; +extern XBT_PUBLIC(int) _sg_mc_sparse_checkpoint; +extern XBT_PUBLIC(int) _sg_mc_ksm; +extern XBT_PUBLIC(int) _sg_mc_soft_dirty; +extern XBT_PUBLIC(char*) _sg_mc_property_file; +extern XBT_PRIVATE int _sg_mc_timeout; +extern XBT_PRIVATE int _sg_mc_hash; +extern XBT_PRIVATE int _sg_mc_max_depth; +extern XBT_PUBLIC(int) _sg_mc_visited; +extern XBT_PRIVATE char* _sg_mc_dot_output_file; +extern XBT_PUBLIC(int) _sg_mc_comms_determinism; +extern XBT_PUBLIC(int) _sg_mc_send_determinism; +extern XBT_PRIVATE int _sg_mc_safety; +extern XBT_PRIVATE int _sg_mc_liveness; +extern XBT_PRIVATE int _sg_mc_snapshot_fds; +extern XBT_PRIVATE int _sg_mc_termination; /********************************* Global *************************************/ -void _mc_cfg_cb_reduce(const char *name, int pos); -void _mc_cfg_cb_checkpoint(const char *name, int pos); -void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos); -void _mc_cfg_cb_property(const char *name, int pos); -void _mc_cfg_cb_timeout(const char *name, int pos); -void _mc_cfg_cb_hash(const char *name, int pos); -void _mc_cfg_cb_snapshot_fds(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); -void _mc_cfg_cb_comms_determinism(const char *name, int pos); -void _mc_cfg_cb_send_determinism(const char *name, int pos); -void _mc_cfg_cb_termination(const char *name, int pos); + +XBT_PRIVATE void _mc_cfg_cb_reduce(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_checkpoint(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_ksm(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_soft_dirty(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_property(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_timeout(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_snapshot_fds(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_hash(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_max_depth(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_visited(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_dot_output(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_comms_determinism(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_send_determinism(const char *name, int pos); +XBT_PRIVATE void _mc_cfg_cb_termination(const char *name, int pos); XBT_PUBLIC(void) MC_run(void); XBT_PUBLIC(void) MC_init(void); XBT_PUBLIC(void) MC_exit(void); XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double); XBT_PUBLIC(double) MC_process_clock_get(smx_process_t); -void MC_automaton_load(const char *file); +XBT_PRIVATE 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_local_variable(const char *var_name, const char *frame); XBT_PUBLIC(void) MC_ignore_global_variable(const char *var_name); -XBT_PUBLIC(void) MC_register_stack_area(void *stack, smx_process_t process, void *context, size_t size); +XBT_PUBLIC(void) MC_register_stack_area(void *stack, smx_process_t process, ucontext_t* context, size_t size); /********************************* Memory *************************************/ XBT_PUBLIC(void) MC_memory_init(void); /* Initialize the memory subsystem */