about summary refs log tree commit diff homepage
path: root/lib/Core/SpecialFunctionHandler.cpp
AgeCommit message (Collapse)Author
2024-01-12new: persistent ptree (-write-ptree) and klee-ptreeFrank Busse
Introduce three different kinds of process trees: 1. Noop: does nothing (e.g. no allocations for DFS) 2. InMemory: same behaviour as before (e.g. RandomPathSearcher) 3. Persistent: similar to InMemory but writes nodes to ptree.db and tracks information such as branch type, termination type or source location (asm) in nodes. Enabled with -write-ptree ptree.db files can be analysed/plotted with the new "klee-ptree" tool.
2023-06-26Remove parentheses around klee_ intrinsics from the help menuCristian Cadar
2023-06-11SpecialFunctionHandler: use std::array for handlerInfoJulian Büning
2023-04-06Support disabling compiler warnings; Use with external headersMartin Nowack
2023-03-23stats: add termination class statsFrank Busse
2022-09-14Support UBSan-enabled binariesPavel Yatcheniy
2022-06-13Update SpecialFunctionHandler.cppChaoqi Zhang
use size() to get N in bind(), just like the way in prepare().
2022-01-05introduce BranchTypesFrank Busse
2022-01-05Remove outdated reference to klee_make_symbolic_nameCristian Cadar
2021-12-23Introduce termination categoriesFrank 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-20Fixed fail with preferCex, removed relation from first argumentTaras Bereznyak
2021-02-16add ifdefs for C++ exception handlingJulian Büning
restoring old behavior without EH support
2020-11-12Casting.h: isa_and_nonnull<>Julian Büning
2020-11-12Ref: implement operator bool()Julian Büning
2020-10-12address MartinNowack's remaining feedbackJulian Büning
2020-10-12Exception handling only for LLVM >= 8.0.0Julian Büning
2020-10-12use 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-12Implemented support for C++ ExceptionsFelix 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-01Use constraint sets and separate metadata for timing solver invocationMartin 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-30Moved 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-30Created include/klee/Core directory and moved appropriate files direc\Cristian Cadar
tly in lib/Core
2020-04-30Removed the Internal directory from include/kleeCristian Cadar
2020-04-08readStringAtAddress: support pointer into objectsMarek 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-08readStringAtAddress: use stringstream to obtain the stringMarek Chalupa
The code is simpler and more in the spirit of C++.
2019-11-28Move merging related code from Executor into MergingSearcherLukas Wölfer
Co-authored-by: Felix Rath <felix.rath@comsys.rwth-aachen.de>
2019-09-03Moved solver-related header files into a separate klee/Solver/ directory.Cristian Cadar
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-04-02Handle __assert() function as handleAssertFail. This assert variant is used ↵Gleb Popov
on FreeBSD
2019-03-15Categorized the options in SpecialFunctionHandler.cppCristian Cadar
2018-11-23Implemented memalign with alignmentLukas Wölfer
2018-10-16Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file is meant ↵Cristian Cadar
to have only solver options.
2018-07-11Removed 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-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-06-13klee_int: allow NULL as nameFrank Busse
2018-06-11Fixed memory leak from Executor::inCloseMerge, fixes #883Lukas Wölfer
2018-05-17Improve error messages for ReadStringAtAddressTimotej Kapus
2018-05-15Implemented incomplete mergingLukas Wölfer
2018-05-05Fix handling of errno if external functions are invokedMartin 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-01fix compilation warningFrank Busse
2017-11-30Implemented bounded merging functionalityLukas Wölfer
2017-11-24klee_make_symbolic: warn on deprecated usageFrank 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-06Removed the word 'unsigned' from integer overflow error messagesAndrew Santosa
2017-08-04Removed merging searchersLukas Wölfer
2017-07-23Remove support for LLVM < 3.4Martin Nowack
Request LLVM 3.4 as minimal requirement for KLEE
2016-08-08Merge pull request #447 from hutoTUM/fix-klee_get_obj_sizeMartinNowack
Fix for klee_get_obj_size() crashing on 64-bit, resolves #446
2016-08-08Fix for klee_get_obj_size() crashing on 64-bit, resolves #446hutoTUM
2016-08-04klee: add exit-on-error-type parameterJiri 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-17Refactoring: Moving klee_warning/_error functions to ErrorHandling in ↵Martin Nowack
Support directory
2015-12-11Reword help description for ``--silent-klee-assume`` command lineDan Liew
flag as suggested by @ccadar
2015-12-11Add command line flag ``--silent-klee-assume``to suppress errors due toValentin Wüstholz
infeasible assumptions.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-24 20:39:40 +0000