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 dac3b6e..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;
 }
@@ -344,8 +356,6 @@ void MSG_task_dsend(msg_task_t task, const char *alias, void_f_pvoid_t cleanup)
   msg_process_t process = MSG_process_self();
   msg_mailbox_t mailbox = MSG_mailbox_get_by_alias(alias);
 
-  /* FIXME: these functions are not traceable */
-
   /* Prepare the task to send */
   t_simdata = task->simdata;
   t_simdata->sender = process;
@@ -358,10 +368,24 @@ void MSG_task_dsend(msg_task_t task, const char *alias, void_f_pvoid_t cleanup)
   t_simdata->comm = NULL;
   msg_global->sent_msg++;
 
+#ifdef HAVE_TRACING
+  int call_end = TRACE_msg_task_put_start(task);
+#endif
+
   /* Send it by calling SIMIX network layer */
   smx_action_t comm = simcall_comm_isend(mailbox, t_simdata->message_size,
                        t_simdata->rate, task, sizeof(void *), NULL, cleanup, NULL, 1);
   t_simdata->comm = comm;
+#ifdef HAVE_TRACING
+    if (TRACE_is_enabled()) {
+      simcall_set_category(comm, task->category);
+    }
+#endif
+
+#ifdef HAVE_TRACING
+  if (call_end)
+    TRACE_msg_task_put_end();
+#endif
 }
 
 /** \ingroup msg_task_usage
@@ -409,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);
 
@@ -640,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