| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
the optimisation that rewrites existing constraints when an equality with a constant is added
|
|
needed by Clang.
|
|
ignore the C++ compiler detected and just use the compiler detected
during the LLVM configure.
|
|
fix travis build of upstream STP and also how KLEE links against STP.
|
|
|
|
|
|
|
|
Cleaner, more efficient timestamps
|
|
pull request.
This reverts commit badffc570e1be6b675dcab7e21829bd029c46287.
|
|
|
|
|
|
|
|
mistake in the last cleanup commit.
|
|
* Removed unused member ShadowObjects in ExecutionState
* Added documentation of members and reorder according to categories
|
|
This function should be used solely in assertion statements and is
intended as a sanity check to make sure that the solution constructed
by IndependentSolver::getInitialValues() produces and answer that in
fact satisfies the the query.
|
|
Previous implementation simply passed the entire constraint forward
without any factoring of the constraint at all. This is a problem
since it is highly likely that there are cached solutions to pieces
of the constraint. The new implementation breaks the entire
constraint down into its requisite factors and passes each piece
forward, one by one, down the solver chain. After an answer is
returned, it is integrated into a larger solution. Since, by
definition, no factor can affect another, we can safely create a
solution to the larger constraint from the answers of its smaller
pieces.
The reconstruction of the solution is done by analyzing which parts of
an array a factor touches. If the factor is the only one to reference
a particular array, then all of the values calculated in the solution
for that array are included in the final answer. If the factor
references a particular element of the array (for example, arr[1]),
then only the value in index 1 of array arr will be included in the
solution.
|
|
This functionality is necessary in order to more effectively handle
calls to IndependentSolver::getInitialValues. An incoming query will
be broken down into its smaller parts, and each piece will be solved
for. At the end, the pieces will be recombined into a larger solution.
The IndependentElementSet::getAllFactors() method takes a query and
breaks it down into all of it's non-interacting factors. The
IndependentElementSet::calculateArrays() method calculates which
arrays are involved in a particular factor.
|
|
|
|
|
|
Use correct definition and declaration of main function
|
|
|
|
|
|
Add some missing header to silence
compiler warnings
|
|
|
|
|
|
|
|
details.
|
|
also test a negative constant as the lhs.
|
|
|
|
|
|
Replaced inefficient llvm::sys::Process::GetTimeUsage() with TimeValue::now(),
because in many cases only the wall clock time is needed, not the user
and sys times (which are significantly more expensive to get).
Updated TimingSolver and WallTimer accordingly.
|
|
[Core] Always warn if states get deleted due to memory limits
|
|
|
|
|
