model-checker : ignore new local variable

[simgrid.git] / src / msg / msg_gos.c

diff --git a/src/msg/msg_gos.c b/src/msg/msg_gos.c
index 682da5b..1b6ac3d 100644 (file)
--- a/src/msg/msg_gos.c
+++ b/src/msg/msg_gos.c
@@ -164,7 +164,7 @@ msg_error_t MSG_process_sleep(double nb_sec)
  *    sometime waiting on all these mailboxes using @ref MSG_comm_waitany. You can find
  *    an example of use of this function in the @ref MSG_examples section.
  *  - Provide a proper patch to implement this functionality back in MSG. That wouldn't be
- *    very difficult actually. Check the function #MSG_mailbox_get_task_ext. During its call to
+ *    very difficult actually. Check the function @ref MSG_mailbox_get_task_ext. During its call to
  *    simcall_comm_recv(), the 5th argument, match_fun, is NULL. Create a function that filters
  *    messages according to the host (that you will pass as sixth argument to simcall_comm_recv()
  *    and that your filtering function will receive as first parameter, and then, the filter could
@@ -321,7 +321,7 @@ XBT_INLINE msg_comm_t MSG_task_isend_with_matching(msg_task_t task, const char *
   t_simdata->comm = comm->s_comm; /* FIXME: is the field t_simdata->comm still useful? */
 #ifdef HAVE_TRACING
     if (TRACE_is_enabled()) {
-      simcall_set_category(comm, task->category);
+      simcall_set_category(comm->s_comm, task->category);
     }
 #endif
 
@@ -433,6 +433,14 @@ 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);
 
@@ -664,7 +672,7 @@ msg_task_t MSG_comm_get_task(msg_comm_t comm)
 }
 
 /**
- * \brief This function is called by SIMIX to copy the data of a comm.
+ * \brief This function is called by SIMIX in kernel mode to copy the data of a comm.
  * \param comm the comm
  * \param buff the data copied
  * \param buff_size size of the buffer