| Age | Commit message (Collapse) | Author |
|---|
|
Propagate ExternalCallPolicy to allow user-based selection.
|
|
Provide an additional argument to select the concretisation policy.
Fix a bug where the concretisation of a shared memory object was visible
across different states by retrieving a writable object state first.
|
|
Use existing `Executor::toConstant()` function to transform a symbolic
byte of an `ObjectState` to its concrete representation.
This will also add constraints if required.
|
|
Before, only partially symbolic variables have been concretized.
Now, every object that is not fully concrete is concretized correctly
this includes fully symbolic objects.
|
|
Before, external changes to symbolic variables have not been propagated
back to their internal representation.
Do a byte-by-byte comparison and update object state if required.
|
|
variables
The test case is based on the example provided by Mingyi Liu from the KLEE
mailing list.
|
|
|
|
|
|
In commit 2b07721, support was added to p-libcxx.inc & p-llvm.inc
for LLVM versions 14+ (in which, apparently, certain build flags
were changed). To detect these recent versions, the variable
LLVM_VERSION_SHORT was compared numerically to "14"-- the intent
obviously being to express "LLVM version 14 or later".
However, in both v-clang.inc & v-llvm.inc, LLVM_VERSION_SHORT
is defined as the concatenation of LLVM_VERSION_MAJOR and
LLVM_VERSION_MINOR. Therefore, on a machine with, say, LLVM
13.0 installed, LLVM_VERSION_SHORT will be "130" which compares
as larger than "14".
This patch changes the comparison to be against "140".
|
|
|
|
|
|
whether the expression is concretised. Also changed a C string argument to std::string.
|
|
with symbolic arguments. It also introduces a new external call policy, where the symbolic inputs are left unconstrained following such a call, useful for certain external calls such as printf.
|
|
symbolic arguments. One of them is currently expected to fail.
|
|
--compress-execution-tree to --compress-exec-tree. Fix an incorrect reference to --write-exec-tree.
|
|
|
|
|
|
|
|
|
|
Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com>
(cherry picked from commit 1ea1a7576300a4da01d925df42db109660ef54d2)
|
|
Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com>
(cherry picked from commit 5d61fb6114bafbf67c59899d15e397684d4ceb28)
|
|
Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com>
(cherry picked from commit 5d9af025ee5a01b1650f11ed0612a10357a98308)
|
|
|
|
|
|
They are not supported anymore for newer LLVM versions.
|
|
The wording changed slightly in newer versions.
Update the test case to support this.
|
|
The optimiser generates different code and calls fwrite directly instead.
|
|
Similar functionality needs to be added using a new pass manager
|
|
Handle like `memalign` for now.
|
|
`Intrinsic::flt_rounds` got removed
|
|
|
|
|
|
|
|
|
|
This automatically lifts old-style pointers to opaque pointers.
More recent versions use opaque pointers automatically and do not need
an explicit enabling.
|
|
Currently, we assume C++11 support being used to by the tested software.
This needs to change if newer C++ standards should be supported.
|
|
Newer compilers use `-std=gnu17` as the default when compiling C code.
Fix all the test cases that violate this behaviour or explicitly request
older standards `-std=c89` where necessary.
|
|
compilers
|
|
|
|
|
|
|
|
To support multiple include directories for c++ header files, use
`%libcxx_includes`. This string contains the `-I` compiler directive for
each include path as well.
Update test cases to use new directive.
|
|
`libc++` include headers are now split between platform dependent and
platform independent code.
Before, only include files for the platform independent code were
considered. Add support to automatically find platform dependent
includes as well.
Simplify the detection of libraries and paths.
Instead of pointing to the `v1` directory, pointing to the include
directory for `-DKLEE_LIBCXX_INCLUDE_PATH` is enough.
Update build script to support this as well.
|
|
|
|
`-DLLVM_ENABLE_PROJECTS` does not include runtimes anymore,
instead a `-DLLVM_ENABLE_RUNTIMES` should be used in addition
|
|
|
|
If an array name ended with a number, adding a number-only suffix could
generate the same name used as part of the solvers.
In the specific testcase `val_1` became solver array `val_111` which
collided with array `val_11` that became `val_111` as well.
Using an `_` as prefix for the suffix, solves that problem in general,
i.e. `val_1` becomes `val_1_11` and `val_11` becomes `val_11_1`.
Fixes #1668
|
|
callers
|
|
|
|
|
