From: degomme <augustin.degomme@unibas.ch>
Date: Mon, 31 Oct 2016 13:35:33 +0000 (+0100)
Subject: Rework how model checking and mmap get enabled/disabled
X-Git-Tag: v3_14~271^2~1
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/11644e1a44c3ff95e0fbd27e63e654ca647b30e8

Rework how model checking and mmap get enabled/disabled

Simplify test: model checking relies on linux-only syscalls such as signalfd,
mremap, so it won't work on anything else.

But do not set HAVE_MMAP to 0 if MC cannot be built, other parts could use it
Courtesy of M. Volat
---

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 255ba48a21..fc13ea5c7d 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -352,16 +352,6 @@ else()
   set(HAVE_THREAD_LOCAL_STORAGE 0)
 endif()
 
-# Our usage of mmap is Linux-specific (flag MAP_ANONYMOUS), but kFreeBSD uses a GNU libc
-IF(HAVE_MMAP AND
-   NOT "${CMAKE_SYSTEM}" MATCHES "Linux" AND 
-   NOT "${CMAKE_SYSTEM}" MATCHES "kFreeBSD" AND 
-   NOT "${CMAKE_SYSTEM}" MATCHES "GNU" AND 
-   NOT  "${CMAKE_SYSTEM}" MATCHES "Darwin")
-  SET(HAVE_MMAP 0)
-  message(STATUS "Warning: MMAP is thought as non functional on this architecture (${CMAKE_SYSTEM})")
-ENDIF()
-
 if(HAVE_MMAP AND HAVE_THREAD_LOCAL_STORAGE)
   SET(HAVE_MMALLOC 1)
 else()
@@ -380,6 +370,11 @@ else()
   SET(HAVE_MALLOCATOR 0)
 endif()
 
+if(enable_model-checking AND NOT "${CMAKE_SYSTEM}" MATCHES "Linux")
+  message(WARNING "Support for model-checking has not been enabled on ${CMAKE_SYSTEM}: disabling it")
+  set(enable_model-checking FALSE)
+  set(HAVE_MC 0)
+endif()
 if(enable_model-checking AND HAVE_MMALLOC)
   SET(HAVE_MC 1)
   include(FindLibunwind)