diff options
| -rw-r--r-- | cmake/modules/FindZ3.cmake | 3 | ||||
| -rw-r--r-- | include/klee/Internal/ADT/DiscretePDF.inc | 42 | ||||
| -rw-r--r-- | lib/Core/ExecutorUtil.cpp | 7 | ||||
| -rw-r--r-- | runtime/CMakeLists.txt | 30 | ||||
| -rw-r--r-- | test/Feature/Vararg.c | 2 |
5 files changed, 46 insertions, 38 deletions
diff --git a/cmake/modules/FindZ3.cmake b/cmake/modules/FindZ3.cmake index b5f90974..999ed14e 100644 --- a/cmake/modules/FindZ3.cmake +++ b/cmake/modules/FindZ3.cmake @@ -20,6 +20,9 @@ endif() # Try to find headers find_path(Z3_INCLUDE_DIRS NAMES z3.h + # For distributions that keep the header files in a `z3` folder, + # for example Fedora's `z3-devel` package at `/usr/include/z3/z3.h` + PATH_SUFFIXES z3 DOC "Z3 C header" ) if (Z3_INCLUDE_DIRS) diff --git a/include/klee/Internal/ADT/DiscretePDF.inc b/include/klee/Internal/ADT/DiscretePDF.inc index 5aee2de5..eb7bd860 100644 --- a/include/klee/Internal/ADT/DiscretePDF.inc +++ b/include/klee/Internal/ADT/DiscretePDF.inc @@ -162,32 +162,32 @@ void DiscretePDF<T>::update(T item, weight_type weight) { template <class T> T DiscretePDF<T>::choose(double p) { - if (p<0.0 || p>=1.0) { + if ((p < 0.0) || (p >= 1.0)) assert(0 && "choose: argument(p) outside valid range"); - } else if (!m_root) { + + if (!m_root) assert(0 && "choose: choose() called on empty tree"); - } else { - weight_type w = (weight_type) (m_root->sumWeights * p); - Node *n = m_root; - - while (1) { - if (n->left) { - if (w<n->left->sumWeights) { - n = n->left; - continue; - } else { - w -= n->left->sumWeights; - } - } - if (w<n->weight || !n->right) { - break; // !n->right condition shouldn't be necessary, just sanity check + + weight_type w = (weight_type) (m_root->sumWeights * p); + Node *n = m_root; + + while (1) { + if (n->left) { + if (w<n->left->sumWeights) { + n = n->left; + continue; + } else { + w -= n->left->sumWeights; } - w -= n->weight; - n = n->right; } - - return n->key; + if (w<n->weight || !n->right) { + break; // !n->right condition shouldn't be necessary, just sanity check + } + w -= n->weight; + n = n->right; } + + return n->key; } template <class T> diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 56f18e6b..b91b5dee 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -153,6 +153,11 @@ namespace klee { case Instruction::FCmp: assert(0 && "floating point ConstantExprs unsupported"); } +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) + llvm_unreachable("Unsupported expression in evalConstantExpr"); +#else + assert(0 && "Unsupported expression in evalConstantExpr"); +#endif + return op1; } - } diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt index 68eb9016..1e680e5d 100644 --- a/runtime/CMakeLists.txt +++ b/runtime/CMakeLists.txt @@ -82,19 +82,11 @@ if (NOT ENV_BINARY) message(FATAL_ERROR "Failed to find env binary") endif() -# Unfortunately `BUILD_ALWAYS` only seems to be supported with the version of ExternalProject -# that shipped with CMake >= 3.1. Should we just avoid using this option? We don't really -# need it unless we are patching gsl itself and need to rebuild. -if (("${CMAKE_VERSION}" VERSION_EQUAL "3.1") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.1")) - option(KLEE_RUNTIME_ALWAYS_REBUILD "Always try to rebuild KLEE runtime" ON) - if (KLEE_RUNTIME_ALWAYS_REBUILD) - set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 1) - else() - set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 0) - endif() +option(KLEE_RUNTIME_ALWAYS_REBUILD "Always try to rebuild KLEE runtime" ON) +if (KLEE_RUNTIME_ALWAYS_REBUILD) + set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG 1) else() - set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "") - message(WARNING "KLEE's runtime will not be automatically rebuilt.") + set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG 0) endif() # Build the runtime as an external project. @@ -106,11 +98,19 @@ ExternalProject_Add(BuildKLEERuntimes SOURCE_DIR "${CMAKE_CURRENT_BINARY_DIR}" BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}" CONFIGURE_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command + BUILD_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command + INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command +) + +# Use `ExternalProject_Add_Step` with `ALWAYS` argument instead of directly +# building in `ExternalProject_Add` with `BUILD_ALWAYS` argument due to lack of +# support for the `BUILD_ALWAYS` argument in CMake < 3.1. +ExternalProject_Add_Step(BuildKLEERuntimes RuntimeBuild # `env` is used here to make sure `MAKEFLAGS` of KLEE's build # is not propagated into the bitcode build system. - BUILD_COMMAND ${ENV_BINARY} MAKEFLAGS="" ${MAKE_BINARY} -f Makefile.cmake.bitcode all - ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} - INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command + COMMAND ${ENV_BINARY} MAKEFLAGS="" ${MAKE_BINARY} -f Makefile.cmake.bitcode all + ALWAYS ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}" ) # FIXME: Invoke `make clean` in the bitcode build system diff --git a/test/Feature/Vararg.c b/test/Feature/Vararg.c index 398ba6f8..82fbe4f1 100644 --- a/test/Feature/Vararg.c +++ b/test/Feature/Vararg.c @@ -12,7 +12,7 @@ struct triple { int first, second, third; }; -int test1(int x, ...) { +void test1(int x, ...) { va_list ap; va_start(ap, x); int i32 = va_arg(ap, int); |