Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
libutil.h header there.
|
|
|
|
|
|
* Use directory instead of libc++ files
* support `bca` and `ba` files
* Add additional checks if directories exist
|
|
|
|
|
|
provides a workaround for LLVM bug PR39177, which affects LLVM
versions 3.9 - 7.0.0: https://bugs.llvm.org/show_bug.cgi?id=39177
This commit is intended to be reverted once support for LLVM
versions <= 7 is dropped from KLEE.
|
|
|
|
|
|
* also adds klee-replay as dependency for systemtests
|
|
So that we do not optimize the library during build. It should be
optimized only on runtime, depending on the -optimize parameter.
It could cause various failures like:
inlinable function call in a function with debug info must have a !dbg location
call void @klee_overshift_check(i64 64, i64 %int_cast_to_i64)
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
runtime
|
|
|
|
|
|
|
|
|
|
|
|
fixes #314
|
|
This target invokes the `clean` target but is also intended for use by
other cleaning targets. The `clean_runtime` target is now declared as a
dependency of `clean-all` so that the runtime is cleaned as well.
|
|
It seems we need to pass `-D` to CMake explicitly.
|
|
to aid debugging.
|
|
`KLEE_SOLVER_LIBRARIES` variables. The code to add `NDEBUG` to
`KLEE_COMPONENT_CXX_DEFINES` did so before initialisation and would
be silently overwritten.
|
|
On FreeBSD <sys/capabilities.h> is present in libc, so we don't require libcap there.
Close and write functions are located in <unistd.h>.
|
|
dynamically based on whether MetaSMT is available. Previously the
default was always off.
|
|
zlib. The default is `ON` if zlib is found on first configure
and `OFF` if zlib is not found on first configure.
|
|
`ENABLE_SOLVER_Z3` to be set dynamically based on whether Z3 is
available. Previously the default was always off.
|
|
`ENABLE_SOLVER_STP` to be set dynamically based on whether STP is
available. Previously the default was always off.
|
|
This could lead to lots of problems. If we discover that these
configurations don't work at all we should make this an error.
|
|
|
|
version and a metaSMT version that requires RTTI
|
|
|
|
`ExternalProject_Add_Step()` so that when using Ninja the output of the
bitcode build system is shown immediately.
|
|
The intention of this option was to provide a switch that can be
used to globally enable/disable tests.
This option ended up causing a lot of confusion as can be seen
on the discussion on writing documention for the new build system.
https://github.com/klee/klee.github.io/pull/53
So it was decided to remove this option. This fixes #568 .
|
|
disallow using reserved target names.
|
|
Surprisingly the old code still worked even when the target didn't
exist.
|
|
This was a proposal from #500.
@andreamattavelli pointed out that the lit tests are really
system tests rather than integration tests so this commit fixes
the inappropriate naming that I chose.
|
|
built with `-fvisibility-inlines-hidden`.
This was observed when using a bottled version of LLVM 3.4 on macOS
that appears to have been built with this option.
|
|
and then re-configured with `ENABLE_TCMALLOC` set to OFF then
`klee/Config/config.h` was not correctly re-generated.
|
|
Remove support for reporting the approximate git tag.
|
|
This was confusing because it would emit something like
`v1.0.0-290-g08d4716` because the 1.1.0 and 1.2.0 releases
didn't have a tag on the master branch so `git describe --tags`
would just find the `v1.0.0` tag and report based on that tag.
|
|
|
|
|
|
to see if we can find klee-uclibc's C library.
|
|
interfering with CMake build.
We now raise a fatal error if we detect certain files in the source
tree. This is a heuristic but it's good enough for now.
The order of includes has also been changed so that the build tree
include directory has priority over the source tree include directory so
that even if the added check was missing the right header file (i.e.
`${CMAKE_BINARY_DIR}/include/klee/Config/config.h` would be picked up at
build time.
|