| Age | Commit message (Collapse) | Author |
|---|
|
|
|
performed with one expressed in terms of number of forks.
|
|
|
|
Some Linux distributions, e.g. Fedora, do not install the unversioned Python
binary by default and Python 2 has been dead for more than a year.
|
|
|
|
It may happen that some older instance of klee is already present
in PATH. All tests that call plain klee instead of %klee may use
it and then unexpectedly fail.
This commit will make all tests that rely on klee tools being
explicitly in PATH fail in our CI. From now on, only LLVM tools,
FileCheck and not will be in lit's PATH.
|
|
CMake 3.19+ started to issue warnings if this policy is set to OLD:
CMake Deprecation Warning at test/CMakeLists.txt:143 (cmake_policy):
The OLD behavior for policy CMP0026 will be removed from a future version
of CMake.
The cmake-policies(7) manual explains that the OLD behaviors of all
policies are deprecated and that a policy should be set to OLD only under
specific short-term circumstances. Projects should be ported to the NEW
behavior and not rely on setting a policy to OLD.
|
|
|
|
|
|
|
|
|
|
f[k], with k symbolic and f a 4-element vector into something along the lines:
if k == 0 => f[0]
elif k == 1 => f[1]
elif k == 2 => f[2]
elif k == 3 => f[3]
else ==> undef
|
|
f[k] = v, with f a 4-element vector, into something along the lines:
if k == 0 => f[0] = v
if k == 1 => f[1] = v
if k == 2 => f[2] = v
if k == 3 => f[3] = v
|
|
the overflow behaviour is different in LLVM 11.
|
|
|
|
System header files on macOS are not part of `/usr/include` since
Catalina. Instead, multiple locations are possible and depend on the
selected SDK.
Use `xcrun` to automatically detect the correct path on macOS.
|
|
|
|
|
|
|
|
|
|
library.
|
|
|
|
This was executing the loop when n==0 leading to an out of bound pointer
error.
Found while verifying Rust code that compares strings.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We implement the Itanium ABI unwinding base-API, and leave the
C++-specific parts to libcxxabi.
Co-authored-by: Lukas Wölfer <lukas.woelfer@rwth-aachen.de>
|
|
|
|
|
|
|
|
with a test case.
|
|
|
|
|
|
|
|
- If an unknown intrinsic appears in the bitcode file,
it is reported but execution can proceed.
- If an unknown intrinsic is encountered during execution of some path,
- the intrinsic is reported
- this path is treated as an error
- execution of other paths can proceed
To be more precise, there is a list of "known unknown intrinsics".
Intrinsics not on this list will prevent execution.
|
|
This is a thread-local version of __cxa_atexit (but, in the absence
of threads, it is sufficient to just call __cxa_atexit).
The test is based on the existing test for atexit in
test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c
The motivation for adding this function is to support the Rust standard
library that calls __cxa_thread_atexit_impl.
This function is usually a weak symbol but, in KLEE, this behaves like a call
to an unknown function and chaos ensues.
Worse, it happens just as the program is cleanly shutting itself down,
so programs that are cleanly exiting crash with the wrong message.
|
|
This instrinsic detects whether the program is being executed
symbolically or concretely (i.e., using the libkleeRuntest library).
The intended usage (illustrated in the test program) is to
allow the test program to display the input values by invoking
any libraries it wants to.
This is especially valuable if you are constructing complex,
structured values and for languages like Rust (or C++) that have
rich libraries and print libraries.
For example, you might pick a symbolic value N with the
assumption "0 <= N < 10" and then pick N symbolic
values and write them to an array.
The resulting ktest file is a bit hard to understand compared with the
output of the standard print function in Rust/C++.
|
|
Changes:
- IntrinsicCleaner accepts fshr/fshl as accepted intrinsics
- Executor::executeCall converts fshr/fshl to urem/zext/concat/shift/extract
- Klee/main suppresses warnings about externals that are LLVM reserved
(i.e., begin with "llvm.")
- New test exercises 32 and 7 bit versions including oversize shift values
Test values are based on LLVM's test for fshl/fshr
- Changes that depend on existence of fshr/fshl are guarded by
#if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0)
or
; REQUIRES: geq-llvm-7.0
|
|
* extend help messages for -max-memory and -max-memory-inhibit
* introduces branchingPermitted()
* enforces fork/branch limits in branch() (vector version)
* changes main loop
* calls updateStates() before checkMemoryUsage()
* calls updateStates() again in case we early terminate states
This should prevent double termination for now. Other solutions are
imho more expensive as we would have to compare possibly large
vectors of states (either states(arr) in checkMemoryUsage() or
removedStates in terminateState()).
|
|
|
|
|
|
|
|
|
|
variadic arguments
|
|
and reformatted comments.
|
|
|
|
byval attribute
|
