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. The 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 AND Libevent_FOUND)
+ message(STATUS "All dependencies found. The stateful model-checking can be enabled.")
+ 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 libevent-dev to enable the stateful 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()
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("")