X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/7a1d9713c8dd8a96686f75acb428b2e4dcb08c1f..1c7a41396837993cb4b8bf91224c5bc458157326:/CMakeLists.txt

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4fa8107700..4acad42269 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -355,48 +355,46 @@ if(enable_model-checking AND minimal-bindings)
   message(FATAL_ERROR "Compile-time option 'minimal-bindings' cannot be enabled with 'model-checking'")
 endif()
 
-if(HAVE_MMAP)
-  SET(HAVE_MMALLOC 1)
-else()
-  SET(HAVE_MMALLOC 0)
-  if(enable_model-checking)
-    message(STATUS "Warning: support for model-checking has been disabled because you are missing either mmap or __thread.")
-  endif()
-  SET(enable_model-checking 0)
-endif()
-
 if(enable_mallocators)
   SET(SIMGRID_HAVE_MALLOCATOR 1)
 else()
   SET(SIMGRID_HAVE_MALLOCATOR 0)
 endif()
 
-find_package(Libevent REQUIRED)
-include_directories(${LIBEVENT_INCLUDE_DIR})
-set(SIMGRID_DEP "${SIMGRID_DEP} ${LIBEVENT_LIBRARIES}")
+SET(SIMGRID_HAVE_MC 0)
+SET(SIMGRID_HAVE_STATEFUL_MC 0)
+SET(HAVE_MMALLOC 0)
+
+find_package(Libevent)
+if(Libevent_FOUND)
+  message(STATUS "Found libevent. Stateless model-checking can be enabled.")
+  include_directories(${LIBEVENT_INCLUDE_DIR})
+  set(SIMGRID_DEP "${SIMGRID_DEP} ${LIBEVENT_LIBRARIES}")
+  SET(SIMGRID_HAVE_MC 1)
+else()
+  message(STATUS "libevent not found. Please install libevent-dev to enable the SimGrid model checker.")
+endif()
 
 if(enable_model-checking)
   include(FindLibunwind)
-  if(HAVE_LIBUNWIND)
-    SET(SIMGRID_DEP "${SIMGRID_DEP} ${LIBUNWIND_LIBRARIES}")
+  find_package(Libdw)
+  find_package(Libelf)
+  if(HAVE_MMAP AND HAVE_LIBUNWIND AND Libdw_FOUND AND Libelf_FOUND)
+    SET(SIMGRID_HAVE_STATEFUL_MC 1)
+    SET(HAVE_MMALLOC 1)
+    SET(SIMGRID_DEP "${SIMGRID_DEP} ${LIBUNWIND_LIBRARIES} ${LIBELF_LIBRARIES} ${LIBDW_LIBRARIES}")
+    include_directories(${LIBDW_INCLUDE_DIR} ${LIBELF_INCLUDE_DIR})
+    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -gdwarf-4")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -gdwarf-4")
   else()
-    message(FATAL_ERROR "Please install libunwind-dev libdw-dev libelf-dev if you want to compile the SimGrid model checker.")
+    message(STATUS "Please install libunwind-dev libdw-dev libelf-dev if you want to compile the SimGrid model checker.")
+    set(HAVE_MMALLOC 0)
   endif()
-  find_package(Libdw REQUIRED)
-  find_package(Libelf REQUIRED)
-  include_directories(${LIBDW_INCLUDE_DIR} ${LIBELF_INCLUDE_DIR})
-  set(SIMGRID_DEP "${SIMGRID_DEP} ${LIBELF_LIBRARIES} ${LIBDW_LIBRARIES}")
-  set(SIMGRID_HAVE_MC 1)
-  set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -gdwarf-4")
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -gdwarf-4")
-else()
-  SET(SIMGRID_HAVE_MC 0)
-  set(HAVE_MMALLOC 0)
 endif()
 mark_as_advanced(PATH_LIBDW_H)
 mark_as_advanced(PATH_LIBDW_LIB)
 
-if (enable_model-checking AND enable_ns3)
+if (SIMGRID_HAVE_MC AND enable_ns3) 
   message(WARNING "Activating both model-checking and ns-3 bindings is considered experimental.")
 endif()
 
@@ -938,7 +936,8 @@ message("        Compile Boost.Context support: ${HAVE_BOOST_CONTEXTS}")
 message("")
 message("        Maintainer mode .............: ${enable_maintainer_mode}")
 message("        Documentation ...............: ${enable_documentation}")
-message("        Model checking ..............: ${SIMGRID_HAVE_MC}")
+message("        Stateless model checking ....: ${SIMGRID_HAVE_MC}")
+message("        Stateful model checking .....: ${SIMGRID_HAVE_STATEFUL_MC}")
 message("        Graphviz mode ...............: ${HAVE_GRAPHVIZ}")
 message("        Mallocators .................: ${enable_mallocators}")
 message("")