From 76cf83f4634017a34173bbceb819b99d77ac7ba7 Mon Sep 17 00:00:00 2001 From: cristianrosa Date: Thu, 20 Jan 2011 15:45:59 +0000 Subject: [PATCH] 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 --- examples/msg/chord/chord.c | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c index 54919e0a6c..6bccfd494d 100644 --- 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 "mc/modelchecker.h" 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); + MC_assert(task_received == task_sent); + 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); + MC_assert(task_received == task_sent); + if (task_received != task_sent) { handle_task(node, task_received); } -- 2.20.1