about summary refs log tree commit diff homepage
path: root/lib/Core
AgeCommit message (Collapse)Author
2019-05-30remove klee_alias_function()Julian Büning
this function can be used to modify the control flow of the program on different paths, enabling self-modifying code.
2019-05-28Implement handling of the llvm.fabs intrinsicFelix Rath
2019-04-04some minor refactoringsFrank Busse
2019-04-04Clean klee-stats, StatsTracker and cmakeTimotej Kapus
2019-04-04Change the .stats format into sqlite3Timotej Kapus
Improves querying of the .stats file, reduces its size, speeds up reads and writes and has better defined fail behaviour.
2019-04-02Handle __assert() function as handleAssertFail. This assert variant is used ↵Gleb Popov
on FreeBSD
2019-04-02Fix build of Executor.cpp on FreeBSD.Gleb Popov
2019-03-21drop support for LLVM <= 3.7Julian Büning
2019-03-21remove obsolete macro KLEE_LLVM_GEP_TYPEJulian 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-16Added support for disabling --batch-instructions and --batch-time by setting ↵Cristian Cadar
them to 0
2019-03-15Placed option categories in the klee namespace and options in the anonymous ↵Cristian Cadar
namespace in Executor.cpp
2019-03-15Placed --max-time in the termination categoryCristian Cadar
2019-03-15Categorized the options in SpecialFunctionHandler.cppCristian Cadar
2019-03-15Added help message for --use-constant-arrays, and placed option in the ↵Cristian Cadar
constraint solving category
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-15Created a new statistics option categoryCristian Cadar
2019-03-13Renamed --red-zone-space to --redzone-size and improved help messageCristian Cadar
2019-03-13Consistently use "default=true" and "default=false" instead of "default=on" ↵Cristian Cadar
and "default=off" in --help
2019-03-13Created new search option category and moved there the options in ↵Cristian Cadar
UserSearcher.cpp
2019-03-13Created a new memory management option category for the options in ↵Cristian Cadar
MemoryManager.cpp
2019-03-13Added --debug-log-state-merge to path merging categoryCristian Cadar
2019-03-12Fixed unitialised memory in `MergeHandler`Martin Nowack
Add missing initialisation for `closedMean` for `MergeHandler`
2019-03-12time: add double type for span multiplicationsFrank Busse
2019-03-11Replaced "default=off" with "default=false"MartinNowack
Co-Authored-By: ccadar <c.cadar@imperial.ac.uk>
2019-03-11Created a path merging option category and improved help message for path ↵Cristian Cadar
merging options
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-05Fixed crash on zero size arraysLukas Wölfer
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