| Age | Commit message (Collapse) | Author |
|---|
|
correctly applied
|
|
constant arrays.
|
|
Added error message when STP fails to fork.
|
|
|
|
Removing unused lib/SMT directory
|
|
|
|
Modify scripts and a test to allow ASan/UBSan builds.
|
|
compiler warnings, one by adding an assert, and the other by refactoring the choose() function.
|
|
Revert "Increased the type size for the stop-after-n-instructions option to a…"
|
|
a…"
|
|
Increased the type size for the stop-after-n-instructions option to a…
|
|
too strict limitations
|
|
Signed-off-by: Levente Kurusa <levex@linux.com>
|
|
Fix Vararg test
|
|
The helper function had int return type, while no value was being
returned.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
|
|
with ASan.
|
|
when using the native compiler in system tests.
This fixes the `libkleeruntest` tests when building with ASan.
|
|
flags.
The old build system stupidly propagates flags for the host C compiler
into the flags for the C bitcode compiler leading to unwanted
instrumentation being added to KLEE's runtime.
|
|
builds
of KLEE.
Two configurations (one for each build system) have been added to
TravisCI to do an ASan build.
|
|
When building with ASan the `mallinfo()` function is intercepted.
However the currently implementation is just a stub that always
returns 0. So instead use the public API of the sanitizer runtime
to get the amount of currently allocated memory when KLEE is built
with ASan.
Unfortunately it appears that the way to detect building with ASan
differs between Clang and GCC. There was also a sanitizer runtime
API change too.
This was tested with
* Clang 3.4, 3.5, and 3.9.0
* GCC 4.8, 4.9, 5.2, 5.4 and, 6.2.1.
|
|
[CMake] Remove `ENABLE_TESTS` CMake cache option.
|
|
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 .
|
|
[CMake] Rename "integrationtests" to "systemtests", removed some undocumented targets and other build changes
|
|
disallow using reserved target names.
|
|
Surprisingly the old code still worked even when the target didn't
exist.
|
|
targets from Autoconf/Makefile build system. Having these around
just confuses things.
|
|
* lit tests are run by the `systemtests` target
* The `check` target runs the `systemtests` and `unittests` target
This make its target names consistent with the CMake build system.
|
|
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.
|
|
Fixes and testing for libkleeRuntest
|
|
Previously error messages would be emitted but execution would continue
which might not be desirable.
Now a wrapper function (for fprintf) `report_internal_error()` is used
which will cause the program to exit. The older behaviour of continuing
to execute after an error can be achieved by setting a new environment
variable `KLEE_RUN_TEST_ERRORS_NON_FATAL`.
This commit also adds a test for each error case.
|
|
If KLEE generates ktest files with `--posix-runtime` then if replaying
using libkleeRuntest then replay would be incorrect because the
`model_version` object would be unintentionally used during replay.
For now just skip over that object and try the next one.
Also emit a warning if the object names don't match.
|
|
test is marked XFAIL because there is a bug in the implementation
of `libkleeRuntest`.
Quite a few changes had to be made to the lit configuration in
order to support these tests.
To run the tests I had to fix #480 for the autoconf/Makefile build
system otherwise the `libkleeRuntest` library would not be found
by the system linker at runtime.
|
|
Brings llvm-ar into line with llvm-as and lli, removing the assumption that
llvm-ar is installed system wide
|
|
1. It expects only 2 arguments, so if linking succeeds, nothing will happen (thanks to []),
otherwise the message "checking for new_bitvector() in -lmetaSMT" will appear.
The latter is that what we currently observe, which means linking actually failed.
2. The reason for linking failure is the use of "-lmetaSMT" in LDFLAGS.
AC_LINK_IFELSE does approximately the following: ${CXX} ... -lmetaSMT ${EXECUTABLE_NAME} ${LIBS},
which causes "libmetaSMT cannot be found" (at least on Ubuntu Xenial, where ${LIBS} = -lz).
After consulting https://www.gnu.org/software/autoconf/manual/autoconf-2.66/html_node/Running-the-Linker.html,
adding "-lmetaSMT" to ${LIBS} seems to be the correct solution.
|
|
|
|
|
|
macOS fixes
|
|
|
|
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.
|
|
Fixes and clean ups in the TravisCI scripts
|
|
When trying to KLEE with a version of LLVM (specifically, 3.5) built from
Github (https://github.com/llvm-mirror/llvm/tree/release_35) the regex in
find_llvm.cmake failed to match the LLVM version string because it was suffixed
with "svn" - i.e. "3.5.2svn".
Added the optional "svn" suffix to the CMake regex to fix this.
|
|
to the root of the build tree after doing the hack the generate
the lit configuration files.
This will make it easier in the future to run more test configurations
(e.g. by passing options to lit to change KLEE's behaviour).
|
|
fast rather than continuing to run the tests (due to `set -e` at the
beginning of the script).
Although this gives less information in the event of a broken build
it means our builds might finish faster if they are broken and it
also simplifies the script significantly.
|
|
even though configure/build failed. This due to using the `&&` operator
which means failure of commands to execute in this compound statement
will not trigger the script to exit as requested by `set -e`.
|
|
Typo fix when compiling with LLVM 3.5 and above
|
|
Replaced an incorrect comma with a semicolon in the Executor constructor.
|
|
[CMake] Fix bug with enabling and then disabling TCMalloc support
|
|
and then re-configured with `ENABLE_TCMALLOC` set to OFF then
`klee/Config/config.h` was not correctly re-generated.
|
|
[CMake] Fix bugs in the Makefile bitcode build system
|
