| Age | Commit message (Collapse) | Author |
|---|
|
controlled by a new parameter `moduleIsFullyLinked`. When
true the linkage type of a weak alias is ignored. It is legal to do
this when the module is fully linked because there won't be another
function that could override the weak alias.
This fixes a previous assertion failure in `klee::getDirectCallTarget()`
triggered by the `test/regression/2016-11-24-bitcast-weak-alias.c` test case.
|
|
`klee::getDirectCallTarget(llvm::CallSite)`.
The problem is that it doesn't handle bitcasted functions that call a
weak alias.
|
|
Silenced warning: comparison of integers of different signs ('const i…
|
|
'const unsigned long long')
|
|
too strict limitations (LLVM >= 3.0)
|
|
|
|
ReadExpr::create() was missing an opportunity to constant fold
|
|
|
|
width greater than 64
|
|
|
|
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.
|
