| Age | Commit message (Collapse) | Author |
|---|
|
a help message.
|
|
|
|
|
|
|
|
|
|
--max-static-... options under the termination category of options
|
|
|
|
|
|
|
|
|
|
|
|
Check if a state reaches the maximum number of stack frames allowed.
To be performant, the number of stack frames are checked.
In comparison, native execution checks the size of the stack.
Still, this is good enough to find possible stack overflows.
The limit can be changed with `-max-stack-frames`. The current
default is 8192 frames.
|
|
--external-calls, updated tests accordingly, and improved documentation on external calls
|
|
CmdLineOptions.cpp are currently added.
|
|
This should not change the behaviour of KLEE and mimics the old API.
- functions moved from util into time namespace
- uses time points and time spans instead of double
- CLI arguments now have the form "3h5min8us"
Changed command line parameters:
- batch-time (double to string)
- istats-write-interval (double to string)
- max-instruction-time (double to string)
- max-solver-time (double to string)
- max-time (double to string)
- min-query-time-to-log (double to string)
- seed-time (double to string)
- stats-write-interval (double to string)
- uncovered-update-interval (double to string)
- added: log-timed-out-queries (replaces negative max-solver-time)
|
|
createLowerSwitchPass moved in llvm commit 49ca55e3813c to Utils.h.
createInstructionCombiningPass moved in llvm commitb5b7fce64c1d to
InstCombine.h. So add the includes where needed.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
In llvm commit 03bcb2143b5c, OpenFlags were split and openFileForWrite
accepts one more parameter. Fortunately, openFileForWrite now defaults
to F_None, so we remove the parameter completely from llvm 3.7 and
later.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Since llvm commit 06d6207c1c63, WriteBitcodeToFile accepts Module &, not
Module *.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Some headers were moved from llvm/Target/ to llvm/CodeGen/. Handle that.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
I.e. klee::printVersion should now have a parameter -- the output
stream. Change both the prototype and the implementation to handle this
properly.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
This was renamed in LLVM commit 54f0462d2b7f, so handle the rename.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Since LLVM 5 commit 1f8f0490690b, CallSite.paramHasAttr is indexed from
0, so make sure we use correct indexing in klee. And use
CallSite.hasRetAttr for return attributes.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Modify the IntrinsicCleaner accordingly.
We do not do anything with the third argument as we do not handle the
first argument in any way.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
In llvm 5, since commit 957caa243d9270df37a566aedae3f1244e7b62ef, the
first parameter to APFloat::convertToInteger is MutableArrayRef. So
handle that.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
llvm 5, moved file_magic to BinaryFormat in commit
19ca2b0f9daed883c21730285d7f04424e5f5f88, so adapt to that.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Starting llvm 5, SwitchInst->findCaseValue() now has to be dereferenced
using ->. So do so, otherwise we see:
../lib/Core/Executor.cpp:1598:38: error: no member named 'getCaseSuccessor' in 'llvm::SwitchInst::CaseIteratorImpl<llvm::SwitchInst::CaseHandle>'; did you mean to use '->' instead of '.'?
BasicBlock *caseSuccessor = i.getCaseSuccessor();
^
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
llvm 5 does not terminate getOrInsertFunction parameters with NULL, take
care of that.
Since commit 9d54400bba7eb04bca80fce97fa170452d19eaf1.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Otherwise we see:
../lib/Expr/Expr.cpp:331:14: error: no member named 'integerPartWidth' in namespace 'llvm'; did you mean 'llvm::APFloatBase::integerPartWidth'?
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
As the shift checker could be executed multiple times, we need to avoid
that shift instructions are instrumented multiple times as well.
Mark the instrumented instruction using metadata and avoid it in
successive runs.
|
|
Do not instrument shift operations with constant shift operations that
are smaller than the type size.
|
|
Use llvm::Builder instead of Inst::Create* to create instruction. This
handles metadata automatically and does instruction folding if possible.
Updated to C++11 and clang-formatted.
|
|
DivChecker can be executed multiple times due to the new linking
process.
Avoid instrumenting div instructions multiple times by annotating
checked instructions with marker. Only unmarked div instructions will be
instrumented.
|
|
Do not instrument divisions which do have a constant non-zero value.
|
|
Use llvm::Builder instead of raw `*Inst::create()` functions.
Builder automatically manages metadata (e.g. debug, TBAA, ..) such that
we don't have to take care of this automatically.
Updated code to C++11 and clang-formated it.
|
|
Simplify the handling of metadata attached to LLVM IR that is specific
to KLEE.
|
|
|
|
and introduce klee_open_compressed_output_file with similar behavior
along some other minor improvements
|
|
|
|
|
|
|
|
|
|
* use `using` instead of typdef
* use `collection.empty()` instead of size
* use `auto` if clear
* use `emplace_back` where useful
* use `nullptr` instead of NULL
* use `override` if applicable
* use `explicit` for constructor to avoid implicit conversion
|
|
Don't pollute the project include directory with optimization specific
headers.
|
|
Remove unneeded headers from include files
|
|
Conditions are checked inside of `optimizeExpr()`
anyway. This simplifies the code a lot.
|
|
|
|
simplifies code a lot.
|
|
avoid ambiguity of valueOnly parameter
|
|
|
|
|
