| Age | Commit message (Collapse) | Author |
|---|
|
satisfiable KLEE doesn't exit with an error.
|
|
The tests don't seem to pass right now.
|
|
docker image.
|
|
build so that it possible to build 32-bit applications.
|
|
with -m32 (i.e. for i386). Previously if this was attempt allocations
in the program being executed by KLEE would hit an assertion because
malloc() would return an address that doesn't fit in a 32-bit pointer.
The interface of MemoryManager has been changed so that it is necessary
to specify the pointer size on creation. The implementation has been
changed to use a MASSIVE HACK when the pointer width is less than
64-bits.
|
|
``__VERIFIER_assert()`` which conflicts with ours. Remove their
implementation if it is detected.
|
|
the --svcomp-runtime flag. This is accompanied with a set of tests
to check all the functions are callable.
Due to the fact that the SV-COMP benchmark suite contains a mixture
of i386 and x86_64 benchmarks it is necessary to compile the runtime
functions twice, once for i386 and once for x86_64 and then link the
right version in at runtime. An example function that is problematic
is ``__VERIFIER_nondet_long()`` which is a different size on i386
and x86_64.
|
|
|
|
Don't use /tmp for futimesat unit test
|
|
This causes problems on a shared machine where multiple users are running the
KLEE unit tests.
|
|
Fix signed division by constant 1/ -1
|
|
Allow to generate initial values for queries with empty constraint set.
|
|
|
|
Travis: Support KLEE with different STP versions, in particular 2.1.0; Disable r940
|
|
Say farewell to r940.
|
|
Build STP version based on provided branch.
Build current STP version 2.1.0 by default and test with master branch
as well
|
|
Division by constant divisor get optimized
using shift and multiplication operations in STP builder.
The used method cannot be applied for divisor 1 and -1.
In that case use slow path.
|
|
Added option to specify a different entry point from main(). Remove some whitespaces.
|
|
Fix assertion failure in getDirectCallTarget
|
|
|
|
|
|
|
|
Added link in README.md to coverage information for KLEE's codebase
|
|
|
|
|
|
Enabling assertions by default for KLEE. While the instructions for …
|
|
explicitely requir assertions to be enabled, in 3.4 we ask users to use LLVM packages, which are built in Release mode. This was prompted by issue #246, where the bug would have resulted in an easier-to-debug assert failure.
|
|
New version of the get initial values functionality which makes use of the independent solver.
|
|
Option --readable-posix-inputs used to turn on/off POSIX-related CEX preferences
|
|
Added an option for the super-set check in CexCachingSolver -- off by default
|
|
The super-set check in the CexCachingSolver takes MUCH longer than the
sub-set check. Upon closer inspection, the super-set check gets slower
and slower as more counterexamples fill the UBTree. Pretty quickly,
the cost of the super-set check becomes larger than the time required
to simply bypass it and go to the Solver.
|
|
Added coverage of the KLEE codebase to Travis CI
|
|
set when COVERAGE is, added the python server script to scripts
|
|
|
|
|
|
Make creation of human readable test cases optional rather than default
|
|
|
|
preferences added in the POSIX model. Removed option --prefer-cex which controlled all CEX preferences.
|
|
Previously, default Klee would go through every byte in a test case
and attempt to bound it to be between 0 and 127, making it human
readable. While this may be useful when attempting to understand Klee,
it also means that the time required to create large test suites was
greatly increased. By making this behavior default off, unsuspecting
users won't incur these additional costs.
|
|
It failed when the function being called is a bitcasted alias.
|
|
s/KLEE_INSTALL_LIB_DIR/KLEE_INSTALL_RUNTIME_DIR/
The new name is more accurrate.
|
|
intended for public use.
|
|
|
|
to ``${PREFIX}/lib/klee/runtime``.
This addresses issue #233
|
|
* We don't need to build the native versions so that is now disabled
* We don't need to install (and hence build) the bytecode archive
library versions of klee-libc or kleeRuntimeIntrinsic for new versions
of LLVM right now (this is kind of messy).
|
|
and kleaver.
|
|
when they are given the --version command line option.
Unfortunately to make the build type and git revision available we
need to check this for every build which means KLEE's support library
will be rebuilt for every build which will slow down incremental builds.
This addresses issue #231
|
|
system.
|
|
|
|
|
