| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
LLVM 3.7 added a PointeeType parameter to GetElementPtrInst::Create.
Let's handle that by a macro called KLEE_LLVM_GEP_TYPE, defined in
Version.h.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
reflect the fact that it simply returns a string
|
|
version that takes an argument a stream
|
|
This is too generic and llvm 6.0 defines DEBUG as follows:
#define DEBUG(X) DEBUG_WITH_TYPE(DEBUG_TYPE, X)
This then results in various build failures where once the macro is
defined, once it is not.
So rename this generic macro to KLEE_ARRAY_DEBUG.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
|
|
|
|
|
|
If an external function in KLEE is invoked, it might update errno.
Previously, the errno specific variable in a state was only updated
if it was part of the executed instructions.
That opened up a timeframe that increased the likelihood of errno being
overwritten by another method call.
This patch fixes two issues:
* the errno of the KLEE process state is updated before the external
function call allowing to detect changes to it later on
* after the external call, the memory object of errno is directly
updated
with its new value, reducing the likelihood to be overwritten by
another
call
Additional features:
* Add support for `errno()` for Darwin as well.
* Simplified errno handling in POSIX layer
|
|
clang 5 reports:
In file included from ../lib/Core/MergeHandler.cpp:10:
../include/klee/MergeHandler.h:81:12: warning: private field 'closedStateCount' is not used [-Wunused-private-field]
unsigned closedStateCount;
^
So fix it by removing the member.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
the old build system (now removed).
|
|
|
|
|
|
Added support for hiding command-line options
|
|
Fixes klee/klee#717
delete on null pointer is always safe.
|
|
|
|
|
|
location as a string. Also added const qualifier to the printFileLine functions
|
|
|
|
|
|
Request LLVM 3.4 as minimal requirement for KLEE
|
|
- having an explicit function which is defined for multiple llvm
versions separately increases readability.
- also: error handling was simplified
- Personal motivation: being able to use this functionality in unit tests
fixes #561
related to #656
|
|
In LLVM 3.7, PassManager was moved to the legacy:: namespace. Introduce
a type for it and use it in the code.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
It became unnecessary when defining options and mainly undefined.
So introduce KLEE_LLVM_CL_VAL_END as suggested by @delcypher.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Fixed typos in comments related to vararg support.
|
|
|
|
|
|
MetaSMTSolver.cpp so that the backend headers only need to be included once there
|
|
`klee_open_output_file()` function so that it can be used by
the Z3Solver.
|
|
assignments against the corresponding `Query` object and check the
assignment evaluates correctly.
This can be switched on using `-debug-assignment-validating-solver`
on the command line.
|
|
finding a bug with the `-exit-on-error` option enabled.
|
|
|
|
It was marked as deprecated long time ago and finally removed in LLVM
3.9. Remove all uses of getGlobalContext and create our own context.
Propagate it all over the code then.
[v2] use ctx, not C as name
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Pass the list as reference. Otherwise we can get errors with newer LLVM
like:
lib/Basic/ConstructSolverChain.cpp:26:19: error: call to deleted constructor of 'llvm::cl::list<QueryLoggingSolverType>'
if (optionIsSet(queryLoggingOptions, SOLVER_KQUERY)) {
^~~~~~~~~~~~~~~~~~~
llvm/Support/CommandLine.h:1466:3: note: 'list' has been explicitly marked deleted here
list(const list &) = delete;
^
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
controlled by a new parameter `moduleIsFullyLinked`. When
true the linkage type of a weak alias is ignored. It is legal to do
this when the module is fully linked because there won't be another
function that could override the weak alias.
This fixes a previous assertion failure in `klee::getDirectCallTarget()`
triggered by the `test/regression/2016-11-24-bitcast-weak-alias.c` test case.
|
|
|
|
width greater than 64
|
|
|
|
compiler warnings, one by adding an assert, and the other by refactoring the choose() function.
|
|
This was confusing because it would emit something like
`v1.0.0-290-g08d4716` because the 1.1.0 and 1.2.0 releases
didn't have a tag on the master branch so `git describe --tags`
would just find the `v1.0.0` tag and report based on that tag.
|
|
* Making `Expr::compre(const Expr&, ExprEquivSet)` private and moving
its implementation into `Expr.cpp`.
* Document `Expr::compare(const Expr&)`.
This partially addresses #515 .
|
|
and make it a pure virtual method. Also make it protected rather than
public because it is an implementation detail of `Expr::compare()`.
This means that sub classes must implement it so this commit also
provides implementations. The comparision behaves as before except
for `ConcatExpr` where its `width` attribute is now used (previously
it wasn't).
This commit also documents the semantics of `Expr::compareContents(const Expr&)`
which was clearly needed because it has been incorrectly implemented
in the past and has gone unnoticed for several years.
This partially addresses #515 .
|
|
`compareContents()`.
This bug would not have affected correctness but it would have
affected performance because if `Expr::compare()` was called on
two structually equal `NotExpr` then its children would be
checked for structually equality twice - once in
NotExpr::compareContents()` and once in `Expr::compare()`.
This partially addresses #515 .
|
|
|
