model-checker : ignore some variables enabled with tracing, and variables about excep...

diff --git a/src/instr/instr_msg_process.c b/src/instr/instr_msg_process.c
index a2d8901..29d321b 100644 (file)
--- a/src/instr/instr_msg_process.c
+++ b/src/instr/instr_msg_process.c
@@ -5,6 +5,7 @@
   * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "instr/instr_private.h"
+#include "mc/mc.h"
 
 #ifdef HAVE_TRACING
 
@@ -28,6 +29,10 @@ void TRACE_msg_process_change_host(msg_process_t process, msg_host_t old_host, m
 {
   if (TRACE_msg_process_is_enabled()){
     static long long int counter = 0;
+
+    if(MC_is_active())
+      MC_ignore_data_bss(&counter, sizeof(counter));
+
     char key[INSTR_DEFAULT_STR_SIZE];
     snprintf (key, INSTR_DEFAULT_STR_SIZE, "%lld", counter++);
 

diff --git a/src/instr/instr_msg_task.c b/src/instr/instr_msg_task.c
index 75b05ba..39da9d7 100644 (file)
--- a/src/instr/instr_msg_task.c
+++ b/src/instr/instr_msg_task.c
@@ -5,6 +5,7 @@
   * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "instr/instr_private.h"
+#include "mc/mc.h"
 
 #ifdef HAVE_TRACING
 
@@ -34,6 +35,12 @@ void TRACE_msg_task_create(msg_task_t task)
   static long long counter = 0;
   task->counter = counter++;
   task->category = NULL;
+  
+  if(MC_is_active()){
+    MC_ignore_data_bss(&counter, sizeof(counter));
+    MC_ignore_heap(&(task->counter), sizeof(task->counter));
+  }
+
   XBT_DEBUG("CREATE %p, %lld", task, task->counter);
 }
 

diff --git a/src/instr/instr_routing.c b/src/instr/instr_routing.c
index e432217..17145b7 100644 (file)
--- a/src/instr/instr_routing.c
+++ b/src/instr/instr_routing.c
@@ -5,6 +5,7 @@
   * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "instr/instr_private.h"
+#include "mc/mc.h"
 
 #ifdef HAVE_TRACING
 #include "surf/surf_private.h"
@@ -117,6 +118,10 @@ static void linkContainers (container_t src, container_t dst, xbt_dict_t filter)
 
   //create the link
   static long long counter = 0;
+
+  if(MC_is_active())
+    MC_ignore_data_bss(&counter, sizeof(counter));
+
   char key[INSTR_DEFAULT_STR_SIZE];
   snprintf (key, INSTR_DEFAULT_STR_SIZE, "%lld", counter++);
   new_pajeStartLink(SIMIX_get_clock(), father, link_type, src, "topology", key);

diff --git a/src/instr/instr_smpi.c b/src/instr/instr_smpi.c
index 65086bd..cd30016 100644 (file)
--- a/src/instr/instr_smpi.c
+++ b/src/instr/instr_smpi.c
@@ -5,6 +5,7 @@
   * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "instr/instr_private.h"
+#include "mc/mc.h"
 #include <ctype.h>
 #include <wchar.h>
 
@@ -87,6 +88,10 @@ static char *TRACE_smpi_put_key(int src, int dst, char *key, int n)
   }
   //generate the key
   static unsigned long long counter = 0;
+  
+  if(MC_is_active())
+    MC_ignore_data_bss(&counter, sizeof(counter));
+
   snprintf(key, n, "%d_%d_%llu", src, dst, counter++);
 
   //push it

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index cc5a4a6..116e5db 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -522,18 +522,18 @@ static int is_stack_ignore_variable(char *frame, char *var_name){
   while(start <= end){
     cursor = (start + end) / 2;
     current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
-    if(strcmp(current_var->frame, frame) == 0){
+    if(strcmp(current_var->frame, frame) == 0 || strcmp(current_var->frame, "*") == 0){
       if(strcmp(current_var->var_name, var_name) == 0)
         return 1;
       if(strcmp(current_var->var_name, var_name) < 0)
         start = cursor + 1;
       if(strcmp(current_var->var_name, var_name) > 0)
         end = cursor - 1;
-    }
-  if(strcmp(current_var->frame, frame) < 0)
+    }else if(strcmp(current_var->frame, frame) < 0){
       start = cursor + 1;
-  if(strcmp(current_var->frame, frame) > 0)
+    }else if(strcmp(current_var->frame, frame) > 0){
       end = cursor - 1; 
+    }
   }
 
   return 0;

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 9f7ae0f..02f1526 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -178,6 +178,16 @@ void MC_init(){
   get_libsimgrid_plt_section();
   get_binary_plt_section();
 
+   /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
+  MC_ignore_stack("e", "*");
+  MC_ignore_stack("__ex_cleanup", "*");
+  MC_ignore_stack("__ex_mctx_en", "*");
+  MC_ignore_stack("__ex_mctx_me", "*");
+  MC_ignore_stack("_log_ev", "*");
+  MC_ignore_stack("_throw_ctx", "*");
+  MC_ignore_stack("ctx", "*");
+
+
   if(raw_mem_set)
     MC_SET_RAW_MEM;
 

diff --git a/src/msg/msg_gos.c b/src/msg/msg_gos.c
index 1b6ac3d..38b579d 100644 (file)
--- a/src/msg/msg_gos.c
+++ b/src/msg/msg_gos.c
@@ -434,13 +434,6 @@ int MSG_comm_test(msg_comm_t comm)
   xbt_ex_t e;
   int finished = 0;
 
-  /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
-  if (MC_is_active()){
-    MC_ignore_stack("e", "MSG_comm_test");
-    MC_ignore_stack("__ex_cleanup", "MSG_comm_test");
-    MC_ignore_stack("__ex_mctx_me", "MSG_comm_test");
-  }
-
   TRY {
     finished = simcall_comm_test(comm->s_comm);
 

diff --git a/src/simix/smx_process.c b/src/simix/smx_process.c
index ad38a71..657c817 100644 (file)
--- a/src/simix/smx_process.c
+++ b/src/simix/smx_process.c
@@ -710,12 +710,6 @@ void SIMIX_process_yield(smx_process_t self)
     SMX_THROW();
   }
 
-  /* Ignore some local variables from xbt/ex.c for stacks comparison */
-  if(MC_is_active()){
-    MC_ignore_stack("ctx", "SIMIX_process_yield");
-    MC_ignore_stack("_throw_ctx", "SIMIX_process_yield");
-    MC_ignore_stack("_log_ev", "SIMIX_process_yield");
-  }
 }
 
 /* callback: context fetching */