| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
compilation.
|
|
|
|
The test contains the program proposed by Eric Rizzi in https://github.com/klee/klee/issues/227, and shows a case in which a constant constraint results after the optimisation.
|
|
Add klee-clang as alternative to klee-gcc
|
|
|
|
always goes to zero (matches LLVM's APInt::ashr(...)). This is meant
to partially address issue #218.
There are a few problems with this commit
* It is possible for AShrExpr to not be abbreviated because the scan
methods will not see that we print the 0th child of the AShrExpr twice
* The added test case should really be run through an SMT solver (
i.e. STP) but that requires infrastructure changes.
|
|
(I'm not sure where python3 came from. I didn't explicitly install it).
Just ship python3.
|
|
/usr/local/bin/ isn't in PATH so using pip after upgrading it fails.
|
|
|
|
klee-stats requires tabulate to be installed.
|
|
This is is tightly coupled with the TravisCI scripts.
There are some really nasty hacks in here that we should get rid of
at some point.
|
|
My first attempt in b41cf33b6b726fd97e502c5c4818f5feeea0284b was wrong
because setting the CC and CXX Makefile variables in Makefile.config.in did not
work because LLVM's Makefile.config would override them.
Also detecting the C compiler is unnecessary because we already do this
(bitcode compiler detection)
|
|
|
|
|
|
runtime was incorrect.
|
