| 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
|
|
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)
|
|
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>
|
|
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>
|
|
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>
|
|
|
|
and introduce klee_open_compressed_output_file with similar behavior
along some other minor improvements
|
|
|
|
Don't pollute the project include directory with optimization specific
headers.
|
|
Conditions are checked inside of `optimizeExpr()`
anyway. This simplifies the code a lot.
|
|
|
|
simplifies code a lot.
|
|
avoid ambiguity of valueOnly parameter
|
|
|
|
|
|
to have only solver options.
|
|
|
|
So handle the type specially whenever needed.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
The rounding was removed because it was never needed:
llvm-mirror/llvm@ff278be
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Link intrinsic library before executing optimizations.
This makes sure that any optimization run by KLEE on the module
is executed for the intrinsic library as well.
Support .ll files as input for KLEE as well.
|
|
|
|
reflect the fact that it simply returns a string
|
|
version that takes an argument a stream
|
|
|
|
dependency --output-istats is not
|
|
|
|
|
|
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
|
|
|
|
doDumpStates calls stepInstruction and therefore indirectly increases time and
instruction statistics for all dangling (dumped) states. This patch removes the
call, but now the timing stats for the last executed state are lost, as
StatsTracker::stepInstruction isn't called anymore.
|
|
|
|
|
|
llvm50 changed the semantics of SwitchInst::CaseIt and started using
"auto" variable type. So use it here too for all versions greater than
3.4 -- 3.4 does not support this semantics yet.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
|
|
|
|
on default searchers
|
