From b436951b74325ab8ba6c798a151cc9081d24153e Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Wed, 31 Oct 2012 18:50:00 +0100 Subject: [PATCH] model-checker : update examples for test snapshot comparison --- examples/msg/mc/test/snapshot_comparison_liveness2.c | 4 +++- examples/msg/mc/test/snapshot_comparison_liveness3.c | 11 +++++++---- examples/msg/mc/test/snapshot_comparison_liveness4.c | 10 ++++++---- examples/msg/mc/test/snapshot_comparison_liveness5.c | 5 +++-- 4 files changed, 19 insertions(+), 11 deletions(-) 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 ****"); -- 2.20.1