X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/be647c10d0b1d760b036f1205f314002637d9876..de2ba1766285962d449105925be099707e0102e6:/src/include/mc/mc.h diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index eca3d4246d..ec2c548791 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -14,6 +14,7 @@ #include "simgrid/simix.h" #include "simgrid/modelchecker.h" /* our public interface (and definition of HAVE_MC) */ #include "xbt/automaton.h" +#include "xbt/dynar.h" #define STD_HEAP_SIZE 20480000 /* Maximum size of the system's heap */ @@ -21,10 +22,14 @@ SG_BEGIN_DECL() extern char*_surf_mc_property_file; /* fixme: better location? */ +extern xbt_dynar_t mc_heap_comparison_ignore; +extern xbt_dynar_t stacks_areas; + /********************************* 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_property(const char *name, int pos); +void _mc_cfg_cb_timeout(const char *name, int pos); XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void); @@ -37,10 +42,19 @@ 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); +/****************************** MC ignore **********************************/ +XBT_PUBLIC(void) MC_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); + /********************************* Memory *************************************/ XBT_PUBLIC(void) MC_memory_init(void); /* Initialize the memory subsystem */ XBT_PUBLIC(void) MC_memory_exit(void); +/* Trigger for state equality detection (check potential cycle in application) */ +void MC_compare(void); + SG_END_DECL() #endif /* _MC_MC_H */