From 4334de1a3cf1c1b19c78fe059b6481a1e53b96c8 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Fri, 29 Jun 2012 15:17:47 +0200 Subject: [PATCH] model-checker : tests for snapshot comparison --- buildtools/Cmake/DefinePackages.cmake | 1 + examples/msg/mc/CMakeLists.txt | 5 + examples/msg/mc/test/compare_snapshot.c | 8 + src/include/mc/mc.h | 3 + src/mc/test/compare_snapshot.c | 263 ++++++++++++++++++++++++ 5 files changed, 280 insertions(+) create mode 100644 examples/msg/mc/test/compare_snapshot.c create mode 100644 src/mc/test/compare_snapshot.c diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index bc69087334..2131344c4c 100644 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -387,6 +387,7 @@ set(MC_SRC src/mc/mc_request.c src/mc/mc_private.h src/mc/mc_liveness.c + src/mc/test/compare_snapshot.c ) set(headers_to_install diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt index 932fca77df..44751fe502 100644 --- a/examples/msg/mc/CMakeLists.txt +++ b/examples/msg/mc/CMakeLists.txt @@ -13,6 +13,8 @@ if(HAVE_MC) add_executable(centralized_liveness centralized_liveness.c) add_executable(centralized_liveness_deadlock centralized_liveness_deadlock.c) add_executable(test_snapshot test_snapshot.c) + add_executable(test/compare_snapshot test/compare_snapshot.c) + target_link_libraries(centralized simgrid m ) target_link_libraries(bugged1 simgrid m ) @@ -24,6 +26,8 @@ if(HAVE_MC) target_link_libraries(centralized_liveness simgrid m ) target_link_libraries(centralized_liveness_deadlock simgrid m ) target_link_libraries(test_snapshot simgrid m ) + target_link_libraries(test/compare_snapshot simgrid m ) + endif(HAVE_MC) set(tesh_files @@ -62,6 +66,7 @@ set(examples_src ${CMAKE_CURRENT_SOURCE_DIR}/bugged2_liveness.h ${CMAKE_CURRENT_SOURCE_DIR}/centralized_liveness.h ${CMAKE_CURRENT_SOURCE_DIR}/test_snapshot.h + ${CMAKE_CURRENT_SOURCE_DIR}/test/compare_snapshot.c PARENT_SCOPE ) set(bin_files diff --git a/examples/msg/mc/test/compare_snapshot.c b/examples/msg/mc/test/compare_snapshot.c new file mode 100644 index 0000000000..fa3d1d2f19 --- /dev/null +++ b/examples/msg/mc/test/compare_snapshot.c @@ -0,0 +1,8 @@ +#include "mc/mc.h" +#include "msg/msg.h" + +int main (int argc, char **argv){ + MSG_init(&argc, argv); + MC_test_snapshot_comparison(); + return 0; +} diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index eca3d4246d..18442d1eb0 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -41,6 +41,9 @@ void MC_automaton_load(const char *file); XBT_PUBLIC(void) MC_memory_init(void); /* Initialize the memory subsystem */ XBT_PUBLIC(void) MC_memory_exit(void); +/********************************* Snapshot comparison test *************************************/ +void MC_test_snapshot_comparison(void); + SG_END_DECL() #endif /* _MC_MC_H */ diff --git a/src/mc/test/compare_snapshot.c b/src/mc/test/compare_snapshot.c new file mode 100644 index 0000000000..59d2e6470a --- /dev/null +++ b/src/mc/test/compare_snapshot.c @@ -0,0 +1,263 @@ +#include "../mc_private.h" + +static void test1(void); +static void test2(void); +static void test2(void); +static void test4(void); +static void test5(void); +static void test6(void); + +static void test1() +{ + + fprintf(stderr, "\n**************** TEST 1 ****************\n\n"); + MC_SET_RAW_MEM; + + /* Save first snapshot */ + mc_snapshot_t snapshot1 = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(snapshot1); + + /* Save second snapshot */ + mc_snapshot_t snapshot2 = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(snapshot2); + + MC_UNSET_RAW_MEM; + + int res = snapshot_compare(snapshot1, snapshot2); + xbt_assert(res == 0); + + fprintf(stderr, "\n**************** END TEST 1 ****************\n"); + + MC_SET_RAW_MEM; + + MC_free_snapshot(snapshot1); + MC_free_snapshot(snapshot2); + + MC_UNSET_RAW_MEM; +} + +static void test2() +{ + + fprintf(stderr, "\n**************** TEST 2 ****************\n\n"); + + MC_SET_RAW_MEM; + + /* Save first snapshot */ + mc_snapshot_t snapshot1 = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(snapshot1); + + MC_UNSET_RAW_MEM; + + char* t = strdup("toto"); + + MC_SET_RAW_MEM; + + /* Save second snapshot */ + mc_snapshot_t snapshot2 = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(snapshot2); + + int res = snapshot_compare(snapshot1, snapshot2); + xbt_assert(res != 0); + + MC_UNSET_RAW_MEM; + + fprintf(stderr, "\n**************** END TEST 2 ****************\n"); + + free(t); + + MC_SET_RAW_MEM; + + MC_free_snapshot(snapshot1); + MC_free_snapshot(snapshot2); + + MC_UNSET_RAW_MEM; +} + +static void test3() +{ + + fprintf(stderr, "\n**************** TEST 3 ****************\n\n"); + + MC_SET_RAW_MEM; + + /* Save first snapshot */ + mc_snapshot_t snapshot1 = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(snapshot1); + + MC_UNSET_RAW_MEM; + + char *t = strdup("toto");; + free(t); + + MC_SET_RAW_MEM; + + /* Save second snapshot */ + mc_snapshot_t snapshot2 = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(snapshot2); + + int res = snapshot_compare(snapshot1, snapshot2); + xbt_assert(res == 0); + + MC_UNSET_RAW_MEM; + + fprintf(stderr, "\n**************** END TEST 3 ****************\n"); + + MC_SET_RAW_MEM; + + MC_free_snapshot(snapshot1); + MC_free_snapshot(snapshot2); + + MC_UNSET_RAW_MEM; +} + +static void test4() +{ + + fprintf(stderr, "\n**************** TEST 4 ****************\n\n"); + + char *t = strdup("toto"); + + MC_SET_RAW_MEM; + + /* Save first snapshot */ + mc_snapshot_t snapshot1 = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(snapshot1); + + MC_UNSET_RAW_MEM; + + free(t); + + MC_SET_RAW_MEM; + + /* Save second snapshot */ + mc_snapshot_t snapshot2 = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(snapshot2); + + int res = snapshot_compare(snapshot1, snapshot2); + xbt_assert(res != 0); + + MC_UNSET_RAW_MEM; + + fprintf(stderr, "\n**************** END TEST 4 ****************\n"); + + MC_SET_RAW_MEM; + + MC_free_snapshot(snapshot1); + MC_free_snapshot(snapshot2); + + MC_UNSET_RAW_MEM; +} + + +static void test5() +{ + + fprintf(stderr, "\n**************** TEST 5 ****************\n\n"); + + char *ptr1 = malloc(sizeof(char *)); + + MC_SET_RAW_MEM; + + /* Save first snapshot */ + mc_snapshot_t snapshot1 = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(snapshot1); + + MC_UNSET_RAW_MEM; + + *ptr1 = *ptr1 + 1; + + MC_SET_RAW_MEM; + + /* Save second snapshot */ + mc_snapshot_t snapshot2 = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(snapshot2); + + int res = snapshot_compare(snapshot1, snapshot2); + xbt_assert(res != 0); + + MC_UNSET_RAW_MEM; + + fprintf(stderr, "\n**************** END TEST 5 ****************\n"); + + MC_SET_RAW_MEM; + + MC_free_snapshot(snapshot1); + MC_free_snapshot(snapshot2); + + MC_UNSET_RAW_MEM; +} + +static void test6() +{ + + fprintf(stderr, "\n**************** TEST 6 ****************\n\n"); + + char *ptr1 = malloc(sizeof(char *)); + + MC_SET_RAW_MEM; + + /* Save first snapshot */ + mc_snapshot_t snapshot1 = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(snapshot1); + + MC_UNSET_RAW_MEM; + + *ptr1 = *ptr1 + 1; + *ptr1 = *ptr1 - 1; + + MC_SET_RAW_MEM; + + /* Save second snapshot */ + mc_snapshot_t snapshot2 = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(snapshot2); + + int res = snapshot_compare(snapshot1, snapshot2); + xbt_assert(res == 0); + + MC_UNSET_RAW_MEM; + + fprintf(stderr, "\n**************** END TEST 6 ****************\n"); + + MC_SET_RAW_MEM; + + MC_free_snapshot(snapshot1); + MC_free_snapshot(snapshot2); + + MC_UNSET_RAW_MEM; +} + + +void MC_test_snapshot_comparison(){ + + MC_memory_init(); + + MC_SET_RAW_MEM; + mc_snapshot_t initial = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(initial); + MC_UNSET_RAW_MEM; + + test1(); + + test2(); + + MC_restore_snapshot(initial); + MC_UNSET_RAW_MEM; + + test3(); + + MC_restore_snapshot(initial); + MC_UNSET_RAW_MEM; + + test4(); + + MC_restore_snapshot(initial); + MC_UNSET_RAW_MEM; + + test5(); + + MC_restore_snapshot(initial); + MC_UNSET_RAW_MEM; + + test6(); +} -- 2.20.1