Age | Commit message (Collapse) | Author | |
---|---|---|---|
2023-06-11 | SpecialFunctionHandler: use std::array for handlerInfo | Julian Büning | |
2023-04-06 | Support disabling compiler warnings; Use with external headers | Martin Nowack | |
2023-03-23 | stats: add termination class stats | Frank Busse | |
2022-09-14 | Support UBSan-enabled binaries | Pavel Yatcheniy | |
2022-06-13 | Update SpecialFunctionHandler.cpp | Chaoqi Zhang | |
use size() to get N in bind(), just like the way in prepare(). | |||
2022-01-05 | introduce BranchTypes | Frank Busse | |
2022-01-05 | Remove outdated reference to klee_make_symbolic_name | Cristian Cadar | |
2021-12-23 | Introduce termination categories | Frank Busse | |
Track all path terminations: esp. for debugging or visualising a persistent process tree (with or without full MoKlee integration) it is helpful to know the exact reason (StateTerminationType) why a path terminated. | |||
2021-11-20 | Fixed fail with preferCex, removed relation from first argument | Taras Bereznyak | |
2021-02-16 | add ifdefs for C++ exception handling | Julian Büning | |
restoring old behavior without EH support | |||
2020-11-12 | Casting.h: isa_and_nonnull<> | Julian Büning | |
2020-11-12 | Ref: implement operator bool() | Julian Büning | |
2020-10-12 | address MartinNowack's remaining feedback | Julian Büning | |
2020-10-12 | Exception handling only for LLVM >= 8.0.0 | Julian Büning | |
2020-10-12 | use isa<> and explicit nullptr-check for compilation with older LLVM ↵ | Felix Rath | |
versions, also mark two errors as ExecErrors, as these should not be caused by users | |||
2020-10-12 | Implemented support for C++ Exceptions | Felix Rath | |
We implement the Itanium ABI unwinding base-API, and leave the C++-specific parts to libcxxabi. Co-authored-by: Lukas Wölfer <lukas.woelfer@rwth-aachen.de> | |||
2020-07-01 | Use constraint sets and separate metadata for timing solver invocation | Martin Nowack | |
Decouple ExecutionState from TimingSolver Instead of providing an execution state to the timing solver use a set of constraints and an additional object for metadata. Fixes: * correct accounting of metadata to a specific state * accounting of all solver invocations (e.g. solver-getRange was not accounted) * allows to invoke the solver without a state (avoids costly copying of states/constraints) | |||
2020-04-30 | Moved header files that were placed directly in include/klee/ into ↵ | Cristian Cadar | |
appropriate existing directories and a new directory Statistics; a few missing renames. | |||
2020-04-30 | Created include/klee/Core directory and moved appropriate files direc\ | Cristian Cadar | |
tly in lib/Core | |||
2020-04-30 | Removed the Internal directory from include/klee | Cristian Cadar | |
2020-04-08 | readStringAtAddress: support pointer into objects | Marek Chalupa | |
The code assumed that the passed pointer points at the beginning of the object. Remove this assumption and support any (constant) pointer. The string is read util either the end of the object is hit (in which case a warning is issued as the string was not zero terminated) or until the terminating zero is found. | |||
2020-04-08 | readStringAtAddress: use stringstream to obtain the string | Marek Chalupa | |
The code is simpler and more in the spirit of C++. | |||
2019-11-28 | Move merging related code from Executor into MergingSearcher | Lukas Wölfer | |
Co-authored-by: Felix Rath <felix.rath@comsys.rwth-aachen.de> | |||
2019-09-03 | Moved solver-related header files into a separate klee/Solver/ directory. | Cristian Cadar | |
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-04-02 | Handle __assert() function as handleAssertFail. This assert variant is used ↵ | Gleb Popov | |
on FreeBSD | |||
2019-03-15 | Categorized the options in SpecialFunctionHandler.cpp | Cristian Cadar | |
2018-11-23 | Implemented memalign with alignment | Lukas Wölfer | |
2018-10-16 | Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file is meant ↵ | Cristian Cadar | |
to have only solver options. | |||
2018-07-11 | Removed support for klee_make_symbolic with 2 arguments. This has been ↵ | Cristian Cadar | |
deprecated for many years now and causes problems during replay. Changed and simplified affected test case. | |||
2018-07-04 | Reorder linking and optimizations | Martin 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-06-13 | klee_int: allow NULL as name | Frank Busse | |
2018-06-11 | Fixed memory leak from Executor::inCloseMerge, fixes #883 | Lukas Wölfer | |
2018-05-17 | Improve error messages for ReadStringAtAddress | Timotej Kapus | |
2018-05-15 | Implemented incomplete merging | Lukas Wölfer | |
2018-05-05 | Fix handling of errno if external functions are invoked | Martin Nowack | |
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 | |||
2018-05-01 | fix compilation warning | Frank Busse | |
2017-11-30 | Implemented bounded merging functionality | Lukas Wölfer | |
2017-11-24 | klee_make_symbolic: warn on deprecated usage | Frank Busse | |
* terminates state instead of using assertion for illegal argument number * renames empty names to "unnamed" (otherwise test generation fails) * deprecates two argument version | |||
2017-10-06 | Removed the word 'unsigned' from integer overflow error messages | Andrew Santosa | |
2017-08-04 | Removed merging searchers | Lukas Wölfer | |
2017-07-23 | Remove support for LLVM < 3.4 | Martin Nowack | |
Request LLVM 3.4 as minimal requirement for KLEE | |||
2016-08-08 | Merge pull request #447 from hutoTUM/fix-klee_get_obj_size | MartinNowack | |
Fix for klee_get_obj_size() crashing on 64-bit, resolves #446 | |||
2016-08-08 | Fix for klee_get_obj_size() crashing on 64-bit, resolves #446 | hutoTUM | |
2016-08-04 | klee: add exit-on-error-type parameter | Jiri Slaby | |
It allows stopping the execution on some conditions like assertions. The use is like: klee -exit-on-error-type=Assert -exit-on-error-type=External file.llvm This is especially useful in the SV-COMP. A test to cover the new parameter was added too. Signed-off-by: Jiri Slaby <jslaby@suse.cz> | |||
2015-12-17 | Refactoring: Moving klee_warning/_error functions to ErrorHandling in ↵ | Martin Nowack | |
Support directory | |||
2015-12-11 | Reword help description for ``--silent-klee-assume`` command line | Dan Liew | |
flag as suggested by @ccadar | |||
2015-12-11 | Add command line flag ``--silent-klee-assume``to suppress errors due to | Valentin Wüstholz | |
infeasible assumptions. | |||
2015-06-03 | Added an option --readable-posix-inputs which is used to turn on/off the CEX ↵ | Cristian Cadar | |
preferences added in the POSIX model. Removed option --prefer-cex which controlled all CEX preferences. | |||
2015-02-13 | refactor integer overflow detection, add signed int | Luca Dariz | |
Instead of checking for every possible casse which result in overflow, it is much simpler to perform the operation using integers with bigger dimension and check if the result overflow |