From 32bc6b382859a96f08f7ef78c0d64efc5235d227 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 4 Sep 2018 11:40:46 -0700 Subject: [PATCH] cmake: Add missing checks for cvc4autoconfig.h to ConfigureCVC4.cmake. --- CMakeLists.txt | 72 +---------------------- cmake/ConfigureCVC4.cmake | 27 +++++++++ cvc4autoconfig.new.h.in | 121 +++++++++----------------------------- 3 files changed, 58 insertions(+), 162 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 47934d05f..264daa615 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -221,8 +221,6 @@ set(CVC4_BUILD_PROFILE_PRODUCTION 0) set(CVC4_BUILD_PROFILE_DEBUG 0) set(CVC4_BUILD_PROFILE_TESTING 0) set(CVC4_BUILD_PROFILE_COMPETITION 0) -# Whether CVC4 is built with the (optional) GPLed library dependences. -set(CVC4_GPL_DEPS 0) #-----------------------------------------------------------------------------# # Compiler flags @@ -338,7 +336,7 @@ if(ENABLE_MUZZLE) endif() if(ENABLE_PORTFOLIO) - find_package(Boost REQUIRED COMPONENTS thread) + find_package(Boost 1.50.0 REQUIRED COMPONENTS thread) # Disable CLN for portfolio builds since it is not thread safe (uses an # unlocked hash table internally). set(USE_CLN OFF) @@ -348,6 +346,7 @@ if(ENABLE_PORTFOLIO) add_c_cxx_flag(-pthread) endif() add_definitions(-DCVC4_PORTFOLIO) + set(BOOST_HAS_THREAD_ATTR 1) endif() if(ENABLE_PROFILING) @@ -459,11 +458,7 @@ if(USE_READLINE) set(HAVE_LIBREADLINE 1) if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR) set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1) - else() - set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 0) endif() -else() - set(HAVE_LIBREADLINE 0) endif() if(USE_SYMFPU) @@ -511,73 +506,10 @@ execute_process( include(ConfigureCVC4) -# Define to 1 if Boost threading library has support for thread attributes -set(BOOST_HAS_THREAD_ATTR 0) # Defined if using the CLN multi-precision arithmetic library. set(CVC4_CLN_IMP ${CVC4_USE_CLN_IMP}) # Defined if using the GMP multi-precision arithmetic library. set(CVC4_GMP_IMP ${CVC4_USE_GMP_IMP}) -## Defined if the requested minimum BOOST version is satisfied -#set(HAVE_BOOST 1) -## Define to 1 if you have -#set(HAVE_BOOST_SYSTEM_ERROR_CODE_HPP 1) -## Define to 1 if you have -#set(HAVE_BOOST_THREAD_HPP 1) -# Defined to 1 if clock_gettime() is supported by the platform. -set(HAVE_CLOCK_GETTIME 1) -# define if the compiler supports basic C++11 syntax -set(HAVE_CXX11 1) -# Define to 1 if you have the declaration of `optreset', and to 0 if you don't. -set(HAVE_DECL_OPTRESET 0) -## Define to 1 if you have the declaration of `strerror_r', and to 0 if you -## don't. -#set(HAVE_DECL_STRERROR_R 1) -## Define to 1 if you have the header file. -#set(HAVE_DLFCN_H 1) -# Define to 1 if you have the header file. -set(HAVE_EXT_STDIO_FILEBUF_H 1) -# Defined to 1 if ffs() is supported by the platform. -set(HAVE_FFS 1) -# Define to 1 if you have the header file. -set(HAVE_GETOPT_H 1) -## Define to 1 if you have the header file. -#set(HAVE_INTTYPES_H 1) -## Define to 1 if you have the `gmp' library (-lgmp). -#set(HAVE_LIBGMP 1) -## Define to 1 if you have the `profiler' library (-lprofiler). -#set(HAVE_LIBPROFILER 0) -# Define to 1 to use libreadline -#set(HAVE_LIBREADLINE 0) -## Define to 1 if you have the `tcmalloc' library (-ltcmalloc). -#set(HAVE_LIBTCMALLOC 0) -## Define to 1 if you have the header file. -#set(HAVE_MEMORY_H 1) -# Defined to 1 if sigaltstack() is supported by the platform. -set(HAVE_SIGALTSTACK 1) -## Define to 1 if you have the header file. -#set(HAVE_STDINT_H 1) -## Define to 1 if you have the header file. -#set(HAVE_STDLIB_H 1) -# Define to 1 if you have the `strerror_r' function. -set(HAVE_STRERROR_R 1) -## Define to 1 if you have the header file. -#set(HAVE_STRINGS_H 1) -## Define to 1 if you have the header file. -#set(HAVE_STRING_H 1) -# Defined to 1 if strtok_r() is supported by the platform. -set(HAVE_STRTOK_R 1) -## Define to 1 if you have the header file. -#set(HAVE_SYS_STAT_H 1) -## Define to 1 if you have the header file. -#set(HAVE_SYS_TYPES_H 1) -# Define to 1 if you have the header file. -set(HAVE_UNISTD_H 1) -## Define to the sub-directory where libtool stores uninstalled libraries. -#set(LT_OBJDIR ".libs/") -## Define to 1 if you have the ANSI C header files. -#set(STDC_HEADERS 1) -# Define to 1 if strerror_r returns char *. -set(STRERROR_R_CHAR_P 1) configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h) include_directories(${CMAKE_CURRENT_BINARY_DIR}) diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake index bd88a2a1d..e3152f5ca 100644 --- a/cmake/ConfigureCVC4.cmake +++ b/cmake/ConfigureCVC4.cmake @@ -1,4 +1,7 @@ include(CheckCXXSourceCompiles) +include(CheckIncludeFile) +include(CheckIncludeFileCXX) +include(CheckSymbolExists) # Check whether "long" and "int64_t" are distinct types w.r.t. overloading. # Even if they have the same size, they can be distinct, and some platforms @@ -34,3 +37,27 @@ check_cxx_source_compiles( if(CVC4_NEED_HASH_UINT64_T_OVERLOAD) add_definitions(-DCVC4_NEED_HASH_UINT64_T) endif() + +check_include_file(unistd.h HAVE_UNISTD_H) +check_include_file_cxx(ext/stdio_filebuf.h HAVE_EXT_STDIO_FILEBUF_H) + +check_symbol_exists(clock_gettime "time.h" HAVE_CLOCK_GETTIME) +check_symbol_exists(ffs "strings.h" HAVE_FFS) +check_symbol_exists(optreset "getopt.h" HAVE_DECL_OPTRESET) +check_symbol_exists(sigaltstack "signal.h" HAVE_SIGALTSTACK) +check_symbol_exists(strerror_r "string.h" HAVE_STRERROR_R) +check_symbol_exists(strtok_r "string.h" HAVE_STRTOK_R) + +# Determine if we have the POSIX (int) or GNU (char *) variant of strerror_r. +check_c_source_compiles( + " + #include + int main(void) + { + char buf[1]; + char c = *strerror_r(0, buf, 0); + return 0; + } + " + STRERROR_R_CHAR_P +) diff --git a/cvc4autoconfig.new.h.in b/cvc4autoconfig.new.h.in index ae66b1421..8fafd62e3 100644 --- a/cvc4autoconfig.new.h.in +++ b/cvc4autoconfig.new.h.in @@ -16,115 +16,52 @@ /* Full release string for CVC4. */ #define CVC4_RELEASE_STRING "@CVC4_RELEASE_STRING@" -/* Define to the full name of this package. */ +/* Full name of this package. */ #define PACKAGE_NAME "@PACKAGE_NAME@" -/* Whether CVC4 is built with the (optional) GPLed library dependences. */ -#define CVC4_GPL_DEPS @CVC4_GPL_DEPS@ +/* Define to 1 if CVC4 is built with (optional) GPLed library dependences. */ +#cmakedefine01 CVC4_GPL_DEPS -/* Defined if using the CLN multi-precision arithmetic library. */ +/* Define to use the CLN multi-precision arithmetic library. */ #cmakedefine CVC4_CLN_IMP -/* Defined if using the GMP multi-precision arithmetic library. */ +/* Define to use the GMP multi-precision arithmetic library. */ #cmakedefine CVC4_GMP_IMP -///* Defined if the requested minimum BOOST version is satisfied */ -//#define HAVE_BOOST @HAVE_BOOST@ +/* Define to 1 if Boost threading library has support for thread attributes. */ +#cmakedefine01 BOOST_HAS_THREAD_ATTR -///* Define to 1 if you have */ -//#define HAVE_BOOST_SYSTEM_ERROR_CODE_HPP -// -///* Define to 1 if you have */ -//#define HAVE_BOOST_THREAD_HPP @HAVE_BOOST_THREAD_HPP@ +/* Define to 1 if `clock_gettime' is supported by the platform. */ +#cmakedefine HAVE_CLOCK_GETTIME -/* Define to 1 if Boost threading library has support for thread attributes */ -#define BOOST_HAS_THREAD_ATTR @BOOST_HAS_THREAD_ATTR@ +/* Define to 1 if the declaration of `optreset' is available. */ +#cmakedefine01 HAVE_DECL_OPTRESET -/* Defined to 1 if clock_gettime() is supported by the platform. */ -#define HAVE_CLOCK_GETTIME @HAVE_CLOCK_GETTIME@ +/* Define to 1 if the header file is available. */ +#cmakedefine01 HAVE_EXT_STDIO_FILEBUF_H -/* define if the compiler supports basic C++11 syntax */ -#define HAVE_CXX11 @HAVE_CXX11@ +/* Define to 1 if `ffs' is supported by the platform. */ +#cmakedefine HAVE_FFS -/* Define to 1 if you have the declaration of `optreset', and to 0 if you - don't. */ -#define HAVE_DECL_OPTRESET @HAVE_DECL_OPTRESET@ +/* Define to 1 to use libreadline. */ +#cmakedefine01 HAVE_LIBREADLINE -///* Define to 1 if you have the declaration of `strerror_r', and to 0 if you -// don't. */ -//#define HAVE_DECL_STRERROR_R @HAVE_DECL_STRERROR_R@ +/* Define to 1 if `sigaltstack' is supported by the platform. */ +#cmakedefine HAVE_SIGALTSTACK -///* Define to 1 if you have the header file. */ -//#define HAVE_DLFCN_H @HAVE_DLFCN_H@ +/* Define to 1 if `strerror_r' is supported by the platform. */ +#cmakedefine01 HAVE_STRERROR_R -///* Define to 1 if you have the header file. */ -//#define HAVE_EXT_STDIO_FILEBUF_H @HAVE_EXT_STDIO_FILEBUF_H@ +/* Define to 1 if `strtok_r' is supported by the platform. */ +#cmakedefine HAVE_STRTOK_R -/* Defined to 1 if ffs() is supported by the platform. */ -#define HAVE_FFS @HAVE_FFS@ +/* Define to 1 if the header file is available. */ +#cmakedefine01 HAVE_UNISTD_H -/* Define to 1 if you have the header file. */ -#define HAVE_GETOPT_H @HAVE_GETOPT_H@ +/* Define to 1 if `rl_completion_entry_function' returns (char *). */ +#cmakedefine01 READLINE_COMPENTRY_FUNC_RETURNS_CHARP -///* Define to 1 if you have the header file. */ -//#define HAVE_INTTYPES_H @HAVE_INTTYPES_H@ - -///* Define to 1 if you have the `gmp' library (-lgmp). */ -//#define HAVE_LIBGMP @HAVE_LIBGMP@ - -///* Define to 1 if you have the `profiler' library (-lprofiler). */ -//#cmakedefine HAVE_LIBPROFILER - -/* Define to 1 to use libreadline */ -#define HAVE_LIBREADLINE @HAVE_LIBREADLINE@ - -///* Define to 1 if you have the `tcmalloc' library (-ltcmalloc). */ -//#cmakedefine HAVE_LIBTCMALLOC - -///* Define to 1 if you have the header file. */ -//#define HAVE_MEMORY_H @HAVE_MEMORY_H@ - -/* Defined to 1 if sigaltstack() is supported by the platform. */ -#define HAVE_SIGALTSTACK @HAVE_SIGALTSTACK@ - -///* Define to 1 if you have the header file. */ -//#define HAVE_STDINT_H @HAVE_STDINT_H@ - -///* Define to 1 if you have the header file. */ -//#define HAVE_STDLIB_H @HAVE_STDLIB_H@ - -/* Define to 1 if you have the `strerror_r' function. */ -#define HAVE_STRERROR_R @HAVE_STRERROR_R@ - -///* Define to 1 if you have the header file. */ -//#define HAVE_STRINGS_H @HAVE_STRINGS_H@ - -///* Define to 1 if you have the header file. */ -//#define HAVE_STRING_H @HAVE_STRING_H@ - -/* Defined to 1 if strtok_r() is supported by the platform. */ -#define HAVE_STRTOK_R @HAVE_STRTOK_R@ - -///* Define to 1 if you have the header file. */ -//#define HAVE_SYS_STAT_H @HAVE_STRTOK_R@ - -///* Define to 1 if you have the header file. */ -//#define HAVE_SYS_TYPES_H @HAVE_SYS_TYPES_H@ - -/* Define to 1 if you have the header file. */ -#define HAVE_UNISTD_H @HAVE_UNISTD_H@ - -///* Define to the sub-directory where libtool stores uninstalled libraries. */ -//#cmakedefine LT_OBJDIR "@LT_OBJDIR@" - -/* Define to 1 if rl_completion_entry_function is declared to return pointer - to char */ -#define READLINE_COMPENTRY_FUNC_RETURNS_CHARP @READLINE_COMPENTRY_FUNC_RETURNS_CHARP@ - -///* Define to 1 if you have the ANSI C header files. */ -//#cmakedefine STDC_HEADERS - -/* Define to 1 if strerror_r returns char *. */ -#define STRERROR_R_CHAR_P @STRERROR_R_CHAR_P@ +/* Define to 1 if `strerror_r' returns (char *). */ +#cmakedefine01 STRERROR_R_CHAR_P #endif /* __CVC4__CVC4AUTOCONFIG_H */ -- 2.30.2