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

[simgrid.git] / src / instr / instr_msg_task.c

diff --git a/src/instr/instr_msg_task.c b/src/instr/instr_msg_task.c
index 423eab3..39da9d7 100644 (file)
--- a/src/instr/instr_msg_task.c
+++ b/src/instr/instr_msg_task.c
@@ -5,15 +5,13 @@
   * 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
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY (instr_msg, instr, "MSG");
 
-/*
- * TRACE_msg_set_task_category: tracing interface function
- */
-void TRACE_msg_set_task_category(m_task_t task, const char *category)
+void TRACE_msg_set_task_category(msg_task_t task, const char *category)
 {
   xbt_assert(task->category == NULL, "Task %p(%s) already has a category (%s).",
       task, task->name, task->category);
@@ -32,16 +30,22 @@ void TRACE_msg_set_task_category(m_task_t task, const char *category)
 }
 
 /* MSG_task_create related function*/
-void TRACE_msg_task_create(m_task_t task)
+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);
 }
 
 /* MSG_task_execute related functions */
-void TRACE_msg_task_execute_start(m_task_t task)
+void TRACE_msg_task_execute_start(msg_task_t task)
 {
   XBT_DEBUG("EXEC,in %p, %lld, %s", task, task->counter, task->category);
 
@@ -49,14 +53,14 @@ void TRACE_msg_task_execute_start(m_task_t task)
     int len = INSTR_DEFAULT_STR_SIZE;
     char str[INSTR_DEFAULT_STR_SIZE];
 
-    container_t process_container = getContainer (instr_process_id(MSG_process_self(), str, len));
-    type_t type = getType ("MSG_PROCESS_STATE", process_container->type);
-    val_t value = getValueByName ("task_execute", type);
+    container_t process_container = PJ_container_get (instr_process_id(MSG_process_self(), str, len));
+    type_t type = PJ_type_get ("MSG_PROCESS_STATE", process_container->type);
+    val_t value = PJ_value_get ("task_execute", type);
     new_pajePushState (MSG_get_clock(), process_container, type, value);
   }
 }
 
-void TRACE_msg_task_execute_end(m_task_t task)
+void TRACE_msg_task_execute_end(msg_task_t task)
 {
   XBT_DEBUG("EXEC,out %p, %lld, %s", task, task->counter, task->category);
 
@@ -64,14 +68,14 @@ void TRACE_msg_task_execute_end(m_task_t task)
     int len = INSTR_DEFAULT_STR_SIZE;
     char str[INSTR_DEFAULT_STR_SIZE];
 
-    container_t process_container = getContainer (instr_process_id(MSG_process_self(), str, len));
-    type_t type = getType ("MSG_PROCESS_STATE", process_container->type);
+    container_t process_container = PJ_container_get (instr_process_id(MSG_process_self(), str, len));
+    type_t type = PJ_type_get ("MSG_PROCESS_STATE", process_container->type);
     new_pajePopState (MSG_get_clock(), process_container, type);
   }
 }
 
 /* MSG_task_destroy related functions */
-void TRACE_msg_task_destroy(m_task_t task)
+void TRACE_msg_task_destroy(msg_task_t task)
 {
   XBT_DEBUG("DESTROY %p, %lld, %s", task, task->counter, task->category);
 
@@ -90,14 +94,14 @@ void TRACE_msg_task_get_start(void)
     int len = INSTR_DEFAULT_STR_SIZE;
     char str[INSTR_DEFAULT_STR_SIZE];
 
-    container_t process_container = getContainer (instr_process_id(MSG_process_self(), str, len));
-    type_t type = getType ("MSG_PROCESS_STATE", process_container->type);
-    val_t value = getValueByName ("receive", type);
+    container_t process_container = PJ_container_get (instr_process_id(MSG_process_self(), str, len));
+    type_t type = PJ_type_get ("MSG_PROCESS_STATE", process_container->type);
+    val_t value = PJ_value_get ("receive", type);
     new_pajePushState (MSG_get_clock(), process_container, type, value);
   }
 }
 
-void TRACE_msg_task_get_end(double start_time, m_task_t task)
+void TRACE_msg_task_get_end(double start_time, msg_task_t task)
 {
   XBT_DEBUG("GET,out %p, %lld, %s", task, task->counter, task->category);
 
@@ -105,19 +109,19 @@ void TRACE_msg_task_get_end(double start_time, m_task_t task)
     int len = INSTR_DEFAULT_STR_SIZE;
     char str[INSTR_DEFAULT_STR_SIZE];
 
-    container_t process_container = getContainer (instr_process_id(MSG_process_self(), str, len));
-    type_t type = getType ("MSG_PROCESS_STATE", process_container->type);
+    container_t process_container = PJ_container_get (instr_process_id(MSG_process_self(), str, len));
+    type_t type = PJ_type_get ("MSG_PROCESS_STATE", process_container->type);
     new_pajePopState (MSG_get_clock(), process_container, type);
 
     char key[INSTR_DEFAULT_STR_SIZE];
     snprintf (key, INSTR_DEFAULT_STR_SIZE, "p%lld", task->counter);
-    type = getType ("MSG_PROCESS_TASK_LINK", getRootType());
-    new_pajeEndLink(MSG_get_clock(), getRootContainer(), type, process_container, "SR", key);
+    type = PJ_type_get ("MSG_PROCESS_TASK_LINK", PJ_type_get_root());
+    new_pajeEndLink(MSG_get_clock(), PJ_container_get_root(), type, process_container, "SR", key);
   }
 }
 
 /* MSG_task_put related functions */
-int TRACE_msg_task_put_start(m_task_t task)
+int TRACE_msg_task_put_start(msg_task_t task)
 {
   XBT_DEBUG("PUT,in %p, %lld, %s", task, task->counter, task->category);
 
@@ -125,15 +129,15 @@ int TRACE_msg_task_put_start(m_task_t task)
     int len = INSTR_DEFAULT_STR_SIZE;
     char str[INSTR_DEFAULT_STR_SIZE];
 
-    container_t process_container = getContainer (instr_process_id(MSG_process_self(), str, len));
-    type_t type = getType ("MSG_PROCESS_STATE", process_container->type);
-    val_t value = getValueByName ("send", type);
+    container_t process_container = PJ_container_get (instr_process_id(MSG_process_self(), str, len));
+    type_t type = PJ_type_get ("MSG_PROCESS_STATE", process_container->type);
+    val_t value = PJ_value_get ("send", type);
     new_pajePushState (MSG_get_clock(), process_container, type, value);
 
     char key[INSTR_DEFAULT_STR_SIZE];
     snprintf (key, INSTR_DEFAULT_STR_SIZE, "p%lld", task->counter);
-    type = getType ("MSG_PROCESS_TASK_LINK", getRootType());
-    new_pajeStartLink(MSG_get_clock(), getRootContainer(), type, process_container, "SR", key);
+    type = PJ_type_get ("MSG_PROCESS_TASK_LINK", PJ_type_get_root());
+    new_pajeStartLink(MSG_get_clock(), PJ_container_get_root(), type, process_container, "SR", key);
   }
 
   return 1;
@@ -147,8 +151,8 @@ void TRACE_msg_task_put_end(void)
     int len = INSTR_DEFAULT_STR_SIZE;
     char str[INSTR_DEFAULT_STR_SIZE];
 
-    container_t process_container = getContainer (instr_process_id(MSG_process_self(), str, len));
-    type_t type = getType ("MSG_PROCESS_STATE", process_container->type);
+    container_t process_container = PJ_container_get (instr_process_id(MSG_process_self(), str, len));
+    type_t type = PJ_type_get ("MSG_PROCESS_STATE", process_container->type);
     new_pajePopState (MSG_get_clock(), process_container, type);
   }
 }