Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-05-30 | remove 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-28 | Implement handling of the llvm.fabs intrinsic | Felix Rath | |
2019-04-04 | some minor refactorings | Frank Busse | |
2019-04-04 | Clean klee-stats, StatsTracker and cmake | Timotej Kapus | |
2019-04-04 | Change the .stats format into sqlite3 | Timotej Kapus | |
Improves querying of the .stats file, reduces its size, speeds up reads and writes and has better defined fail behaviour. | |||
2019-04-02 | Handle __assert() function as handleAssertFail. This assert variant is used ↵ | Gleb Popov | |
on FreeBSD | |||
2019-04-02 | Fix build of Executor.cpp on FreeBSD. | Gleb Popov | |
2019-03-21 | drop support for LLVM <= 3.7 | Julian Büning | |
2019-03-21 | remove obsolete macro KLEE_LLVM_GEP_TYPE | Julian Büning | |
2019-03-19 | Add support to assign debug instructions to optimised code | Martin Nowack | |
2019-03-19 | Use debugging information from newer LLVM versions | Martin Nowack | |
2019-03-19 | Refactor InstructionInfoTable | Martin Nowack | |
Better debug information | |||
2019-03-17 | run VerifierPass after optimization and instrumentation | Julian Büning | |
2019-03-16 | Added support for disabling --batch-instructions and --batch-time by setting ↵ | Cristian Cadar | |
them to 0 | |||
2019-03-15 | Placed option categories in the klee namespace and options in the anonymous ↵ | Cristian Cadar | |
namespace in Executor.cpp | |||
2019-03-15 | Placed --max-time in the termination category | Cristian Cadar | |
2019-03-15 | Categorized the options in SpecialFunctionHandler.cpp | Cristian Cadar | |
2019-03-15 | Added help message for --use-constant-arrays, and placed option in the ↵ | Cristian Cadar | |
constraint solving category | |||
2019-03-15 | Renamed --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-15 | Reformatted options and headers in Executor.cpp and did a proofreading pass ↵ | Cristian Cadar | |
over all help messages. | |||
2019-03-15 | Added several options in Executor.cpp to the constraint solving category | Cristian Cadar | |
2019-03-15 | Created a new statistics option category | Cristian Cadar | |
2019-03-13 | Renamed --red-zone-space to --redzone-size and improved help message | Cristian Cadar | |
2019-03-13 | Consistently use "default=true" and "default=false" instead of "default=on" ↵ | Cristian Cadar | |
and "default=off" in --help | |||
2019-03-13 | Created new search option category and moved there the options in ↵ | Cristian Cadar | |
UserSearcher.cpp | |||
2019-03-13 | Created a new memory management option category for the options in ↵ | Cristian Cadar | |
MemoryManager.cpp | |||
2019-03-13 | Added --debug-log-state-merge to path merging category | Cristian Cadar | |
2019-03-12 | Fixed unitialised memory in `MergeHandler` | Martin Nowack | |
Add missing initialisation for `closedMean` for `MergeHandler` | |||
2019-03-12 | time: add double type for span multiplications | Frank Busse | |
2019-03-11 | Replaced "default=off" with "default=false" | MartinNowack | |
Co-Authored-By: ccadar <c.cadar@imperial.ac.uk> | |||
2019-03-11 | Created a path merging option category and improved help message for path ↵ | Cristian Cadar | |
merging options | |||
2019-03-11 | Add support for LLVM 8.0 | Martin Nowack | |
2019-03-05 | Renamed "Starting options" to "Startup options" and added a missing space in ↵ | Cristian Cadar | |
a help message. | |||
2019-03-05 | fix Executor::initializeGlobals for aliases pointing to another alias | Julian Büning | |
2018-12-19 | Added debugging category | Cristian Cadar | |
2018-12-19 | Renamed --stop-after-n-instructions to --max-instructions, as suggested by @251 | Cristian Cadar | |
2018-12-19 | Added some descriptions suggested by @MartinNowack and placed ↵ | Cristian Cadar | |
--max-static-... options under the termination category of options | |||
2018-12-19 | Added option categories for external call policy and termination criteria | Cristian Cadar | |
2018-12-19 | Created two more option categories: test generation and seeding. | Cristian Cadar | |
2018-11-23 | Implemented memalign with alignment | Lukas Wölfer | |
2018-11-07 | Fix bug which resulted in an incorrect warning to be printed. | Cristian Cadar | |
2018-11-05 | Fixed crash on zero size arrays | Lukas Wölfer | |
2018-11-05 | Check for stack overflow in a tested program | Martin 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-02 | Replaced --no-externals and --allow-external-sym-calls with ↵ | Cristian Cadar | |
--external-calls, updated tests accordingly, and improved documentation on external calls | |||
2018-10-30 | Base time API upon std::chrono | Frank 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-26 | llvm5: CallSite.paramHasAttr is indexed from 0 | Jiri 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-26 | llvm5: use MutableArrayRef for APFloat::convertToInteger | Jiri 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-26 | llvm5: SwitchInst case functions now return pointers | Jiri 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-24 | Added lowering pass | Rafael Zaehl | |
2018-10-23 | refactor klee_open_output_file to return std::unique_ptr | Julian Büning | |
and introduce klee_open_compressed_output_file with similar behavior along some other minor improvements |