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 2ceacc2..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
@@ -294,7 +294,9 @@ XBT_INLINE msg_comm_t MSG_task_isend_with_matching(msg_task_t task, const char *
   msg_process_t process = MSG_process_self();
   msg_mailbox_t mailbox = MSG_mailbox_get_by_alias(alias);
 
-  /* FIXME: these functions are not traceable */
+#ifdef HAVE_TRACING
+  int call_end = TRACE_msg_task_put_start(task);
+#endif
 
   /* Prepare the task to send */
   t_simdata = task->simdata;
@@ -317,6 +319,16 @@ XBT_INLINE msg_comm_t MSG_task_isend_with_matching(msg_task_t task, const char *
     simcall_comm_isend(mailbox, t_simdata->message_size,
                          t_simdata->rate, task, sizeof(void *), match_fun, NULL, match_data, 0);
   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->s_comm, task->category);
+    }
+#endif
+
+#ifdef HAVE_TRACING
+  if (call_end)
+    TRACE_msg_task_put_end();
+#endif
 
   return comm;
 }
@@ -421,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);
 
@@ -652,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