diff options
| -rw-r--r-- | .travis.yml | 9 | ||||
| -rwxr-xr-x | .travis/metaSMT.sh | 11 | ||||
| -rw-r--r-- | cmake/find_metasmt.cmake | 47 | ||||
| -rw-r--r-- | runtime/POSIX/fd.c | 3 | ||||
| -rw-r--r-- | test/CMakeLists.txt | 2 |
5 files changed, 21 insertions, 51 deletions
diff --git a/.travis.yml b/.travis.yml index a0b5e7ae..cd2a9771 100644 --- a/.travis.yml +++ b/.travis.yml @@ -23,6 +23,7 @@ env: # LLVM : {2.9, 3.4} # SOLVERS : {Z3, STP, STP:Z3, metaSMT} # STP_VERSION : {2.1.2, master} + # METASMT_VERSION : {v4.rc1} # METASMT_DEFAULT : {btor, stp, z3} # UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled # DISABLE_ASSERTIONS: {0, 1} @@ -43,7 +44,7 @@ env: # Check KLEE CMake build in a few configurations - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 - - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 + - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 - LLVM_VERSION=2.9 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 # ASan build. Do unoptimized build otherwise the optimizer might remove problematic code @@ -64,9 +65,9 @@ env: - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 # Test metaSMT support - - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - + - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + # Check at least one build with Asserts disabled. - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0 diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh index 8e1cb341..9c21d341 100755 --- a/.travis/metaSMT.sh +++ b/.travis/metaSMT.sh @@ -4,14 +4,9 @@ sudo apt-get -y install libboost1.55-dev libz3 libz3-dev libgmp-dev # Clone -git clone git://github.com/hoangmle/metaSMT.git +git clone -b ${METASMT_VERSION} --single-branch --depth 1 https://github.com/hoangmle/metaSMT.git cd metaSMT -## FIXME: define and use an environment variable METASMT_VERSION instead, when a proper version of metaSMT is available -git checkout 1f9e399 -git clone git://github.com/agra-uni-bremen/dependencies.git -cd dependencies -git checkout 45bc658 -cd .. +git submodule update --init --depth 1 source ${KLEE_SRC}/.travis/sanitizer_flags.sh if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then @@ -22,7 +17,7 @@ fi # Bootstrap export BOOST_ROOT=/usr sudo cp dependencies/Z3-2.19/Z3Config.cmake /usr # this is a hack -./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off --build stp-git-basic --build boolector-2.2.0 --build minisat-git --build lingeling-ayv-86bf266-140429 -DZ3_DIR=/usr +./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off -DmetaSMT_REQUIRE_CXX11=off --build stp-git-basic --build boolector-2.2.0 --build minisat-git --build lingeling-ayv-86bf266-140429 -DZ3_DIR=/usr sudo cp deps/boolector-2.2.0/lib/* /usr/lib/ # sudo cp deps/lingeling-ayv-86bf266-140429/lib/* /usr/lib/ # sudo cp deps/minisat-git/lib/* /usr/lib/ # hack diff --git a/cmake/find_metasmt.cmake b/cmake/find_metasmt.cmake index a0a02cb9..6751b31d 100644 --- a/cmake/find_metasmt.cmake +++ b/cmake/find_metasmt.cmake @@ -18,46 +18,17 @@ list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS # FIXME: We should test linking list(APPEND KLEE_SOLVER_LIBRARIES ${metaSMT_LIBRARIES}) -# THIS IS HORRIBLE. The ${metaSMT_CXXFLAGS} variable -# is badly formed. It is a string but we can't just split -# on spaces because its contents looks like this -# " -DmetaSMT_BOOLECTOR_1_API -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS". -# So handle defines specially -string_to_list("${metaSMT_CXXFLAGS}" _metaSMT_CXXFLAGS_broken_list) -list(LENGTH _metaSMT_CXXFLAGS_broken_list _metaSMT_CXXFLAGS_broken_list_length) -math(EXPR _metaSMT_CXXFLAGS_broken_list_last_index "${_metaSMT_CXXFLAGS_broken_list_length} -1") +# Separate flags and defines from ${metaSMT_CXXFLAGS} +string_to_list("${metaSMT_CXXFLAGS}" _metaSMT_CXXFLAGS_list) set(_metasmt_flags "") set(_metasmt_defines "") -set(_index_to_skip "") -foreach (index RANGE 0 ${_metaSMT_CXXFLAGS_broken_list_last_index}) - list(FIND _index_to_skip "${index}" _should_skip) - if ("${_should_skip}" EQUAL "-1") - list(GET _metaSMT_CXXFLAGS_broken_list ${index} _current_flag) - if ("${_current_flag}" MATCHES "^-D") - # This is a define - if ("${_current_flag}" MATCHES "^-D$") - # This is a bad define. We have just `-D` and the next item - # is the actually definition. - if ("${index}" EQUAL "${_metaSMT_CXXFLAGS_broken_list_last_index}") - message(FATAL_ERROR "Stray -D flag!") - else() - # Get next value - math(EXPR _next_index "${index} + 1") - list(GET _metaSMT_CXXFLAGS_broken_list ${_next_index} _next_flag) - if ("${_next_flag}" STREQUAL "") - message(FATAL_ERROR "Next flag shouldn't be empty!") - endif() - list(APPEND _metasmt_defines "-D${_next_flag}") - list(APPEND _index_to_skip "${_next_index}") - endif() - else() - # This is well formed defined (e.g. `-DHELLO`) - list(APPEND _metasmt_defines "${_current_flag}") - endif() - else() - # Regular flag - list(APPEND _metasmt_flags "${_current_flag}") - endif() +foreach (flag ${_metaSMT_CXXFLAGS_list}) + if ("${flag}" MATCHES "^-D") + # This is a define + list(APPEND _metasmt_defines "${flag}") + else() + # Regular flag + list(APPEND _metasmt_flags "${flag}") endif() endforeach() diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c index 24b248e3..6f78c747 100644 --- a/runtime/POSIX/fd.c +++ b/runtime/POSIX/fd.c @@ -37,6 +37,9 @@ int klee_get_errno(void); /* Returns pointer to the symbolic file structure fs the pathname is symbolic */ static exe_disk_file_t *__get_sym_file(const char *pathname) { + if (!pathname) + return NULL; + char c = pathname[0]; unsigned i; diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index a2a46e2a..4b6a63f6 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -96,7 +96,7 @@ if (DOWNLOAD_NOT_SOURCE) target_include_directories("not" PRIVATE ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS}) target_compile_options("not" PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) target_compile_definitions("not" PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) - target_link_libraries("not" PRIVATE ${FILECHECK_NEEDED_LIBS}) + target_link_libraries("not" PRIVATE ${NOT_NEEDED_LIBS}) endif() ############################################################################### |