about summary refs log tree commit diff homepage
path: root/lib/Core/Executor.cpp
AgeCommit message (Collapse)Author
2019-05-28Implement handling of the llvm.fabs intrinsicFelix Rath
2019-04-02Fix build of Executor.cpp on FreeBSD.Gleb Popov
2019-03-21drop support for LLVM <= 3.7Julian Büning
2019-03-19Add support to assign debug instructions to optimised codeMartin Nowack
2019-03-19Use debugging information from newer LLVM versionsMartin Nowack
2019-03-19Refactor InstructionInfoTableMartin Nowack
Better debug information
2019-03-17run VerifierPass after optimization and instrumentationJulian Büning
2019-03-15Placed option categories in the klee namespace and options in the anonymous ↵Cristian Cadar
namespace in Executor.cpp
2019-03-15Renamed --seed-out to --seed-file and --seed-out-dir to --seed-dir, and ↵Cristian Cadar
placed them in the seeding category. Moved options and option categories in Executor.cpp to the klee namespace.
2019-03-15Reformatted options and headers in Executor.cpp and did a proofreading pass ↵Cristian Cadar
over all help messages.
2019-03-15Added several options in Executor.cpp to the constraint solving categoryCristian Cadar
2019-03-13Consistently use "default=true" and "default=false" instead of "default=on" ↵Cristian Cadar
and "default=off" in --help
2019-03-12time: add double type for span multiplicationsFrank Busse
2019-03-11Add support for LLVM 8.0Martin Nowack
2019-03-05Renamed "Starting options" to "Startup options" and added a missing space in ↵Cristian Cadar
a help message.
2019-03-05fix Executor::initializeGlobals for aliases pointing to another aliasJulian Büning
2018-12-19Added debugging categoryCristian Cadar
2018-12-19Renamed --stop-after-n-instructions to --max-instructions, as suggested by @251Cristian Cadar
2018-12-19Added some descriptions suggested by @MartinNowack and placed ↵Cristian Cadar
--max-static-... options under the termination category of options
2018-12-19Added option categories for external call policy and termination criteriaCristian Cadar
2018-12-19Created two more option categories: test generation and seeding.Cristian Cadar
2018-11-23Implemented memalign with alignmentLukas Wölfer
2018-11-07Fix bug which resulted in an incorrect warning to be printed.Cristian Cadar
2018-11-05Check for stack overflow in a tested programMartin Nowack
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.
2018-11-02Replaced --no-externals and --allow-external-sym-calls with ↵Cristian Cadar
--external-calls, updated tests accordingly, and improved documentation on external calls
2018-10-30Base time API upon std::chronoFrank Busse
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)
2018-10-26llvm5: CallSite.paramHasAttr is indexed from 0Jiri Slaby
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>
2018-10-26llvm5: use MutableArrayRef for APFloat::convertToIntegerJiri Slaby
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>
2018-10-26llvm5: SwitchInst case functions now return pointersJiri Slaby
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>
2018-10-24Added lowering passRafael Zaehl
2018-10-23refactor klee_open_output_file to return std::unique_ptrJulian Büning
and introduce klee_open_compressed_output_file with similar behavior along some other minor improvements
2018-10-23use klee_open_output_file for uncompressed logsJulian Büning
2018-10-23Move optimization specific headers away from the project include directoryMartin Nowack
Don't pollute the project include directory with optimization specific headers.
2018-10-23Remove condition check before function invocationMartin Nowack
Conditions are checked inside of `optimizeExpr()` anyway. This simplifies the code a lot.
2018-10-23Move ConstantExpr check inside optimizeExpr functionMartin Nowack
2018-10-23optimizeExpr: return the result as return value instead as function argumentMartin Nowack
simplifies code a lot.
2018-10-23Make valueOnly parameter of optimizeExpr explicitMartin Nowack
avoid ambiguity of valueOnly parameter
2018-10-23Added support for KLEE value-based array optimizationAndrea Mattavelli
2018-10-23Added support for KLEE index-based array optimizationAndrea Mattavelli
2018-10-16Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file is meant ↵Cristian Cadar
to have only solver options.
2018-09-30Fix a crash when the last running state is terminated during mergingLukas Wölfer
2018-09-18llvm4: PointerType is not SequentialTypeJiri Slaby
So handle the type specially whenever needed. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-18llvm4: APFloat members are functionsJiri Slaby
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-14llvm: make KLEE compile against LLVM 3.9Jiri Slaby
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-07-12llvm38: no rounding in APFloatJiri Slaby
The rounding was removed because it was never needed: llvm-mirror/llvm@ff278be Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-07-04Reorder linking and optimizationsMartin Nowack
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.
2018-05-24remove switch fallthrough in floating point comparisionDaniel Schemmel
2018-05-22Renamed printFileLine to getSourceLocation (as suggested by @delcypher) to ↵Cristian Cadar
reflect the fact that it simply returns a string
2018-05-22Simplified printFileLine by using std::to_string, and removed unneeded ↵Cristian Cadar
version that takes an argument a stream
2018-05-21fix some casts for LLP64 compilersFrank Busse
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-04-20 18:16:10 +0000