Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/simgrid/simgrid
authorPaul Bédaride <paul.bedaride@gmail.com>
Mon, 17 Dec 2012 10:04:19 +0000 (11:04 +0100)
committerPaul Bédaride <paul.bedaride@gmail.com>
Mon, 17 Dec 2012 10:04:19 +0000 (11:04 +0100)
1  2 
src/mc/mc_global.c

diff --combined src/mc/mc_global.c
@@@ -24,12 -24,12 +24,12 @@@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_glob
  e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
  
  
 -extern int _surf_init_status;
 +extern int _sg_init_status;
  void _mc_cfg_cb_reduce(const char *name, int pos) {
 -  if (_surf_init_status && !_surf_do_model_check) {
 +  if (_sg_init_status && !_sg_do_model_check) {
      xbt_die("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
    }
 -  char *val= xbt_cfg_get_string(_surf_cfg_set, name);
 +  char *val= xbt_cfg_get_string(_sg_cfg_set, name);
    if (!strcasecmp(val,"none")) {
      mc_reduce_kind = e_mc_reduce_none;
    } else if (!strcasecmp(val,"dpor")) {
  }
  
  void _mc_cfg_cb_checkpoint(const char *name, int pos) {
 -  if (_surf_init_status && !_surf_do_model_check) {
 +  if (_sg_init_status && !_sg_do_model_check) {
      xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
    }
 -  _surf_mc_checkpoint = xbt_cfg_get_int(_surf_cfg_set, name);
 +  _surf_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
  }
  void _mc_cfg_cb_property(const char *name, int pos) {
 -  if (_surf_init_status && !_surf_do_model_check) {
 +  if (_sg_init_status && !_sg_do_model_check) {
      xbt_die("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
    }
 -  _surf_mc_property_file= xbt_cfg_get_string(_surf_cfg_set, name);
 +  _surf_mc_property_file= xbt_cfg_get_string(_sg_cfg_set, name);
  }
  
  void _mc_cfg_cb_timeout(const char *name, int pos) {
 -  if (_surf_init_status && !_surf_do_model_check) {
 +  if (_sg_init_status && !_sg_do_model_check) {
      xbt_die("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
    }
 -  _surf_mc_timeout= xbt_cfg_get_int(_surf_cfg_set, name);
 +  _surf_mc_timeout= xbt_cfg_get_int(_sg_cfg_set, name);
  }
  
  void _mc_cfg_cb_max_depth(const char *name, int pos) {
 -  if (_surf_init_status && !_surf_do_model_check) {
 +  if (_sg_init_status && !_sg_do_model_check) {
      xbt_die("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
    }
 -  _surf_mc_max_depth= xbt_cfg_get_int(_surf_cfg_set, name);
 +  _surf_mc_max_depth= xbt_cfg_get_int(_sg_cfg_set, name);
  }
  
  void _mc_cfg_cb_visited(const char *name, int pos) {
 -  if (_surf_init_status && !_surf_do_model_check) {
 +  if (_sg_init_status && !_sg_do_model_check) {
      xbt_die("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
    }
 -  _surf_mc_visited= xbt_cfg_get_int(_surf_cfg_set, name);
 +  _surf_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
  }
  
  
@@@ -237,11 -237,11 +237,11 @@@ void MC_modelcheck_safety(void
    initial_state_safety->snapshot = MC_take_snapshot();
    MC_UNSET_RAW_MEM;
  
+   MC_dpor();
    if(raw_mem_set)
      MC_SET_RAW_MEM;
  
-   MC_dpor();
    MC_exit();
  }
  
@@@ -820,6 -820,32 +820,32 @@@ void MC_ignore_data_bss(void *address, 
      MC_SET_RAW_MEM;
  }
  
+ static size_t data_bss_ignore_size(void *address){
+   unsigned int cursor = 0;
+   int start = 0;
+   int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
+   mc_data_bss_ignore_variable_t var;
+   while(start <= end){
+     cursor = (start + end) / 2;
+     var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
+     if(var->address == address)
+       return var->size;
+     if(var->address < address){
+       if((void *)((char *)var->address + var->size) > address)
+         return (char *)var->address + var->size - (char*)address;
+       else
+         start = cursor + 1;
+     }
+     if(var->address > address)
+       end = cursor - 1;   
+   }
+   return 0;
+ }
  void MC_ignore_stack(const char *var_name, const char *frame){
    
    int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@@ -1647,31 -1673,6 +1673,6 @@@ void print_local_variables(xbt_dict_t l
  
  }
  
- static size_t data_bss_ignore_size(void *address){
-   unsigned int cursor = 0;
-   int start = 0;
-   int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
-   mc_data_bss_ignore_variable_t var;
-   while(start <= end){
-     cursor = (start + end) / 2;
-     var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
-     if(var->address == address)
-       return var->size;
-     if(var->address < address){
-       if((void *)((char *)var->address + var->size) > address)
-         return (char *)var->address + var->size - (char*)address;
-       else
-         start = cursor + 1;
-     }
-     if(var->address > address)
-       end = cursor - 1;   
-   }
-   return 0;
- }
  static void MC_get_global_variables(char *elf_file){
  
    FILE *fp;