model-checker : update MSG bugged mutual exclusion example

[simgrid.git] / src / mc / mc_checkpoint.c

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 1ad751d..4b4c43c 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -24,7 +24,8 @@ void *start_data_libsimgrid, *start_bss_libsimgrid;
 void *start_data_binary, *start_bss_binary;
 void *start_text_binary;
 
-/* Free functions */
+/************************************  Free functions **************************************/
+/*****************************************************************************************/
 
 static void MC_snapshot_stack_free(mc_snapshot_stack_t s){
   if(s){
@@ -50,7 +51,8 @@ static void local_variable_free_voidp(void *v){
 }
 
 
-/* Snapshot regions */
+/*******************************  Snapshot regions ********************************/
+/*********************************************************************************/
 
 static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size)
 {
@@ -369,7 +371,8 @@ void MC_get_binary_plt_section(){
 
 }
 
-/* Snapshot */
+/************************************* Take Snapshot ************************************/
+/****************************************************************************************/
 
 static void MC_get_hash_global(char *snapshot_hash, void *data1, void *data2){
   
@@ -489,16 +492,20 @@ static xbt_dynar_t MC_get_local_variables_values(void *stack_context){
   int frame_found = 0, region_type;
   void *frame_pointer_address = NULL;
   long true_ip, value;
+  int stop;
 
   xbt_dynar_t variables = xbt_dynar_new(sizeof(local_variable_t), local_variable_free_voidp);
 
-  while(ret >= 0){
+  while(ret >= 0 && !stop){
 
     unw_get_reg(&c, UNW_REG_IP, &ip);
     unw_get_reg(&c, UNW_REG_SP, &sp);
 
     unw_get_proc_name(&c, frame_name, sizeof (frame_name), &off);
 
+    if(!strcmp(frame_name, "smx_ctx_sysv_wrapper")) /* Stop before context switch with maestro */
+      stop = 1;
+
     if((long)ip > (long)start_text_libsimgrid)
       frame = xbt_dict_get_or_null(mc_local_variables_libsimgrid, frame_name);
     else
@@ -686,6 +693,27 @@ static xbt_dynar_t MC_take_snapshot_ignore(){
 
 }
 
+static void MC_dump_checkpoint_ignore(mc_snapshot_t snapshot){
+  
+  unsigned int cursor = 0;
+  mc_checkpoint_ignore_region_t region;
+  size_t offset;
+  
+  xbt_dynar_foreach(mc_checkpoint_ignore, cursor, region){
+    if(region->addr > snapshot->regions[0]->start_addr && (char *)(region->addr) < (char *)snapshot->regions[0]->start_addr + STD_HEAP_SIZE){
+      offset = (char *)region->addr - (char *)snapshot->regions[0]->start_addr;
+      memset((char *)snapshot->regions[0]->data + offset, 0, region->size);
+    }else if(region->addr > snapshot->regions[2]->start_addr && (char *)(region->addr) < (char*)snapshot->regions[2]->start_addr + snapshot->regions[2]->size){
+      offset = (char *)region->addr - (char *)snapshot->regions[2]->start_addr;
+      memset((char *)snapshot->regions[2]->data + offset, 0, region->size);
+    }else if(region->addr > snapshot->regions[1]->start_addr && (char *)(region->addr) < (char*)snapshot->regions[1]->start_addr + snapshot->regions[1]->size){
+      offset = (char *)region->addr - (char *)snapshot->regions[1]->start_addr;
+      memset((char *)snapshot->regions[1]->data + offset, 0, region->size);
+    }
+  }
+
+}
+
 
 mc_snapshot_t MC_take_snapshot(){
 
@@ -707,6 +735,8 @@ mc_snapshot_t MC_take_snapshot(){
     //MC_get_hash_local(snapshot->hash_local, snapshot->stacks);
   }
 
+  MC_dump_checkpoint_ignore(snapshot);
+
   MC_UNSET_RAW_MEM;
 
   if(raw_mem)