Add assertions to use with the model-checker

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/simgrid/simgrid/trunk@9465 48e7efb5-ca39-0410-a469-dd3cf9ba447f

diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c
index 54919e0..6bccfd4 100644 (file)
--- a/examples/msg/chord/chord.c
+++ b/examples/msg/chord/chord.c
@@ -9,6 +9,7 @@
 #include "msg/msg.h"
 #include "xbt/log.h"
 #include "xbt/asserts.h"
 #include "msg/msg.h"
 #include "xbt/log.h"
 #include "xbt/asserts.h"

+#include "mc/modelchecker.h"

 XBT_LOG_NEW_DEFAULT_CATEGORY(msg_chord,
                              "Messages specific for this msg example");
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(msg_chord,
                              "Messages specific for this msg example");
 


@@ -641,6 +642,8 @@ static int remote_find_successor(node_t node, int ask_to, int id)
         DEBUG1("Received a task (%p)", task_received);
         task_data_t ans_data = MSG_task_get_data(task_received);
 
         DEBUG1("Received a task (%p)", task_received);
         task_data_t ans_data = MSG_task_get_data(task_received);
 

+        MC_assert(task_received == task_sent);
+

         if (task_received != task_sent) {
           // this is not the expected answer
           handle_task(node, task_received);
         if (task_received != task_sent) {
           // this is not the expected answer
           handle_task(node, task_received);


@@ -716,6 +719,8 @@ static int remote_get_predecessor(node_t node, int ask_to)
         m_task_t task_received = MSG_comm_get_task(node->comm_receive);
         task_data_t ans_data = MSG_task_get_data(task_received);
 
         m_task_t task_received = MSG_comm_get_task(node->comm_receive);
         task_data_t ans_data = MSG_task_get_data(task_received);
 

+        MC_assert(task_received == task_sent);
+

         if (task_received != task_sent) {
           handle_task(node, task_received);
         }
         if (task_received != task_sent) {
           handle_task(node, task_received);
         }