model-checker : add local variables from xbt/ex.h in ignore mechanism for stacks...

diff --git a/src/msg/msg_gos.c b/src/msg/msg_gos.c
index 9f2156e..24babd3 100644 (file)
--- a/src/msg/msg_gos.c
+++ b/src/msg/msg_gos.c
@@ -433,6 +433,13 @@ int MSG_comm_test(msg_comm_t comm)
 {
   xbt_ex_t e;
   int finished = 0;
 {
   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");
+  }
+

   TRY {
     finished = simcall_comm_test(comm->s_comm);
 
   TRY {
     finished = simcall_comm_test(comm->s_comm);
 

diff --git a/src/simix/smx_process.c b/src/simix/smx_process.c
index b1db2f4..ad38a71 100644 (file)
--- a/src/simix/smx_process.c
+++ b/src/simix/smx_process.c
@@ -710,7 +710,7 @@ void SIMIX_process_yield(smx_process_t self)
     SMX_THROW();
   }
 
     SMX_THROW();
   }
 

-  /* Ignore some local variables from xbt/ex.c" */
+  /* 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");
   if(MC_is_active()){
     MC_ignore_stack("ctx", "SIMIX_process_yield");
     MC_ignore_stack("_throw_ctx", "SIMIX_process_yield");