about summary refs log tree commit diff homepage
path: root/lib/Core
AgeCommit message (Collapse)Author
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
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-10-10fix handling of failing external callsFrank Busse
Currently KLEE only handles the first segfault in external calls as it doesn't unblock SIGSEGV afterwards. This patch unblocks the signal and enables handling of multiple failing calls.
2018-10-03Marking resolve methods as constCristian Cadar
2018-10-03Refactored AddressSpace::resolve() by creating a new function ↵Cristian Cadar
AddressSpace::checkPointerInObject() that is called in both the forward and the backward searches. This makes the code more modular and removes a large part of duplicated code and should also address the non-deterministic coverage in the resolve() function which affects Codecov reports.
2018-09-30Fix a crash when the last running state is terminated during mergingLukas Wölfer
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-07-14 22:57:00 +0000