model-checker : tests for snapshot comparison

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index bc69087..2131344 100644 (file)
--- 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/mc_request.c
   src/mc/mc_private.h
   src/mc/mc_liveness.c

+  src/mc/test/compare_snapshot.c

   )
 
 set(headers_to_install
   )
 
 set(headers_to_install

diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt
index 932fca7..44751fe 100644 (file)
--- 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(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 )
 
   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(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
 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}/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
   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 (file)
index 0000000..fa3d1d2
--- /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 eca3d42..18442d1 100644 (file)
--- 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);
 
 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 */
 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 (file)
index 0000000..59d2e64
--- /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();
+}