| Age | Commit message (Collapse) | Author |
|---|
|
Will redo the merge to preserve original commits.
This reverts commit a743d7072d9ccf11f96e3df45f25ad07da6ad9d6.
|
|
and mul operations. Refactored tests into two main cases, and
disabled them on LLVM 2.9, which does not support -fsanitized=*signed-integer-overflow.
|
|
Fix va args passing for big types
|
|
|
|
klee: let user override path to runtime library
|
|
ExprSMTLIBPrinter
|
|
|
|
|
|
This patch introduces nested let-abbreviations in the ExprSMTLIBPrinter
to reduce the size of the SMTLIBv2 queries and the corresponding processing
time (bugfix for #170).
The current implementation of the let abbreviation mode does not consider
expression intra-dependencies and prints all abbreviations in the same
let scope. For a (simplified) example, it prints
(assert (let ( (?B1 (A + B)) (?B2 (A + B + C)) ) (= ?B1 ?B2) ) ).
This is extremely inefficient if the expressions (and there many of these!)
extensively reuse their subexpressions. Therefore, it's better to print
the query with nested let-expressions by reusing existing expression bindings
in the new let scope:
(assert (let ( (?B1 (A + B)) ) (let ( (?B2 (?B1 + C)) ) (= ?B1 ?B2) ) ) ).
This patch adds a new function ExprSMTLIBPrinter::scanBindingExprDeps() that
scans bindings for expression dependencies. The result is a vector of
new bindings (orderedBindings) that represents the expression dependency tree.
When printing in the let-abbreviation mode, the new code starts with
abbreviating expressions that have no dependencies and then gradually makes
these new bindings available in the upcoming let-scopes where expressions
with dependencies reuse them.
The effect of nested let-abbreviations is comparable to :named abbreviations.
However, the latter mode is not supported by the majority of the solvers.
|
|
Fix overshift check
|
|
Handling overshift behaviour in MetaSMTBuilder
|
|
Shifting by bitwidth-1 is valid
|
|
Fixed test /Feature/PreferCex.c: Z3 instantiates different value for unc...
|
|
|
|
unconstrained buf[3]
|
|
unordered_map and unordered_set from leaking out into other compilation
units. This should be removed entirely when C++11 support lands.
|
|
|
|
|
|
single method with two different implementations.
There is one version of this method for human readability
(printHumanReadableQuery()) and a version for machine consumption
(printMachineReadableQuery()).
The reason for having two versions is because different behaviour is
needed in different scenarios
* In machine readable mode the entire query is printed inside a single
``(assert ...)``. This is done to allow ``(let ...)`` to abbreviate
as much as possible.
* In human readable mode each constraint and query expression is printed
inside its own ``(assert ...)`` unless the abbreviation mode is
ABBR_LET in which case all constraints and query expr are printed
inside a single ``(assert ...)`` much like in the machine readable mode
Whilst I was here I also fixed a bug handling identation when printing
``(let ...)`` expressions in printAssert()
|
|
* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET)
* Remove the now defunct ExprSMTLIBLetPrinter
* Improve performance of ExprSMTLIBPrinter::scan() by keeping
track of visited Expr to avoid visiting them again
* Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr()
|
|
When looking for runtime library, look first
into KLEE_RUNTIME_LIBRARY_PATH environment variable.
This allows to use klee not only in 'hardcoded' environment.
Signed-off-by: Marek Chalupa <mchqwerty@gmail.com>
|
|
|
|
tools: prepend DESTDIR when installing
|
|
Some tools prepend DESTDIR properly, some not. ktest-tool and
klee-stats do not, so 'make install' chokes with an error:
llvm[2]: Installing Release+Asserts /usr/bin/ktest-tool
/usr/bin/install: cannot create regular file '/usr/bin/ktest-tool': Permission denied
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Allow stp installed in root
|
|
configure/Makefile code that adds Boost as a depdendency because We
don't need to support old versions of STP that needed Boost.
|
|
I have stp in standard paths: /usr/include and /usr/lib64. Allow that
by correct STP_CFLAGS + STP_LDFLAGS instead of STP_ROOT. Those are
empty when --with-stp is not passed.
configure is regenerated by autoconf too.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
Switch to using autoconf 2.69 this version is more commonly available
|
|
willemp/willem/fix_64bit_printing_bug_in_testingUtils
Fix 64bit printing bug in testing utils
|
|
on Linux systems (2.60 is quite old) which will make updating the
configure script easier for most users.
|
|
|
|
Changed _testingUtils to use stdint.h
|
|
The difference between a 64bit pointer truncated to 32 bits and the
original 64bit pointer would never be 0 if any of the high 32bits in
the pointer were test. If lli and klee had a different value for the
top 32bits of the address this test would be marked as failing.
Due to the 64bit printing buf in _testingUtils this was not exposed before.
The fix clears the top 32bits of the difference.
|
|
64bit numbers)
Fixing this bug will expose a failing test case for Concrete/ConstantExpr.ll
|
|
Removed XFAIL tag from the Feature/VarArgLongDouble.c test
Fixed Executor to (more) correctly handle the alignment of types larger than 64bit (such as long double) when those are passed in var_args on x86_64.
Specifically:
From http://www.x86-64.org/documentation/abi.pdf
AMD64-ABI 3.5.7p5: Step 7.
Align l->overflow_arg_area upwards to a 16 byte boundary if alignment needed by type exceeds 8 byte boundary.
|
|
varargs on x86_64.
|
|
This could be useful if KLEE tests want to use the bitcode compiler
as a native compiler.
|
|
Fixes support for passing arguments to klee in the ConcreteTests.
|
|
This is for use with llvm-lit --param=klee_opts=...
Fixes lit.cfg to not have an extranous space behind the klee command.
Augments ConcreteTest to accept and pass arguments to klee.
Augments all the ConcreteTest cases to wrap %klee in quotes.
Without wrapping %klee the extra arguments will be seens as arguments
to ConcreteTest.py resulting in an unknown argument error.
|
|
not 3.0."
|
|
by @hpalikareva).
|
|
MemoryBuffer from the std::unique_ptr when getLazyBitcodeModule()
succesfully takes ownership.
|
|
|
|
The commit that caused this is r202052.
|
|
|
|
|
|
|
|
was removed by r210803
|
|
assertion entirely?
|
|
Generate fake files for test cases
|
