From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Wed, 31 Oct 2012 17:50:00 +0000 (+0100)
Subject: model-checker : update examples for test snapshot comparison
X-Git-Tag: v3_9_rc1~91^2~126^2~24
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/b436951b74325ab8ba6c798a151cc9081d24153e

model-checker : update examples for test snapshot comparison
---

diff --git a/examples/msg/mc/test/snapshot_comparison_liveness2.c b/examples/msg/mc/test/snapshot_comparison_liveness2.c
index 969ee85340..e81f3f8a65 100644
--- a/examples/msg/mc/test/snapshot_comparison_liveness2.c
+++ b/examples/msg/mc/test/snapshot_comparison_liveness2.c
@@ -24,7 +24,7 @@ int test(int argc, char **argv){
   MSG_process_sleep(1);
 
   char *toto = xbt_malloc(5);
-  XBT_INFO("Toto value %s", toto);
+  XBT_INFO("Toto allocated");
 
   void *snap2 = MC_snapshot();
 
@@ -36,6 +36,8 @@ int test(int argc, char **argv){
   
   XBT_INFO("**** End test ****");
 
+  xbt_free(toto);
+
   return 0;
 }
 
diff --git a/examples/msg/mc/test/snapshot_comparison_liveness3.c b/examples/msg/mc/test/snapshot_comparison_liveness3.c
index fdf8966abd..27703a7a4c 100644
--- a/examples/msg/mc/test/snapshot_comparison_liveness3.c
+++ b/examples/msg/mc/test/snapshot_comparison_liveness3.c
@@ -19,23 +19,26 @@ int test(int argc, char **argv){
   XBT_INFO("**** Start test ****");
   XBT_INFO("Malloc and free after first snapshot");
 
+  char *toto = NULL;
+
   void *snap1 = MC_snapshot();
 
   MSG_process_sleep(1);
 
-  char *toto = NULL;
   toto = xbt_malloc(5);
-  XBT_INFO("Toto value %s", toto);
+  XBT_INFO("Toto allocated");
   xbt_free(toto);
   toto = NULL;
+  XBT_INFO("Toto free");
 
   MSG_process_sleep(1);
 
   void *snap2 = MC_snapshot();
 
-  int res = MC_compare_snapshots(snap1, snap2);
+  MC_ignore_stack("snap2", "test");   
+  MC_ignore_stack("snap1", "test");
 
-  XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", res);
+  XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
   
   XBT_INFO("**** End test ****");
 
diff --git a/examples/msg/mc/test/snapshot_comparison_liveness4.c b/examples/msg/mc/test/snapshot_comparison_liveness4.c
index f116228f20..9c38d3072c 100644
--- a/examples/msg/mc/test/snapshot_comparison_liveness4.c
+++ b/examples/msg/mc/test/snapshot_comparison_liveness4.c
@@ -20,21 +20,23 @@ int test(int argc, char **argv){
   XBT_INFO("Free after first snapshot");
   
   char *toto = xbt_malloc(5);
-  XBT_INFO("Toto value %s", toto);
+  XBT_INFO("Toto allocated");
 
   void *snap1 = MC_snapshot();
 
   MSG_process_sleep(1);
 
   xbt_free(toto);
+  XBT_INFO("Toto free");
 
   void *snap2 = MC_snapshot();
 
   MSG_process_sleep(1);
+  
+  MC_ignore_stack("snap2", "test");   
+  MC_ignore_stack("snap1", "test");
 
-  int res = MC_compare_snapshots(snap1, snap2);
-
-  XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", res);
+  XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
   
   XBT_INFO("**** End test ****");
 
diff --git a/examples/msg/mc/test/snapshot_comparison_liveness5.c b/examples/msg/mc/test/snapshot_comparison_liveness5.c
index acb72d1f46..e8054f7e72 100644
--- a/examples/msg/mc/test/snapshot_comparison_liveness5.c
+++ b/examples/msg/mc/test/snapshot_comparison_liveness5.c
@@ -33,9 +33,10 @@ int test(int argc, char **argv){
 
   MSG_process_sleep(1);
 
-  int res = MC_compare_snapshots(snap1, snap2);
+  MC_ignore_stack("snap2", "test");   
+  MC_ignore_stack("snap1", "test");
 
-  XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", res);
+  XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
   
   XBT_INFO("**** End test ****");