X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/1af04af978a0d15f9e4e16db1270e42ff0fc6d11..7baa77e301b3581d4107cbbaab44183aa6b9b918:/src/include/mc/mc.h diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 8be2fd4e74..84169bdc77 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -1,4 +1,5 @@ -/* Copyright (c) 2008-2012. Da SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2014. The SimGrid Team. + * All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ @@ -16,7 +17,7 @@ #include "xbt/automaton.h" #include "xbt/dynar.h" -#define STD_HEAP_SIZE 20480000 /* Maximum size of the system's heap */ +#define STD_HEAP_SIZE (50*1024*1024) /* Maximum size of the system's heap */ SG_BEGIN_DECL() @@ -27,6 +28,7 @@ extern char* _sg_mc_property_file; extern int _sg_mc_timeout; extern int _sg_mc_max_depth; extern int _sg_mc_visited; +extern char* _sg_mc_dot_output_file; extern xbt_dynar_t mc_heap_comparison_ignore; extern xbt_dynar_t stacks_areas; @@ -40,6 +42,7 @@ 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); @@ -54,17 +57,14 @@ 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); +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); 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 */