about summary refs log tree commit diff homepage
path: root/lib/Core/SpecialFunctionHandler.cpp
AgeCommit message (Collapse)Author
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.
2015-06-03Added 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-13refactor integer overflow detection, add signed intLuca 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
2015-02-13Detect overflow of unsigned add, sub and mul operationsLuca Dariz
This requires clang with -fsanitize=unsigned-integer-overflow tested with clang and llvm 3.4.2
2015-02-13Revert "Merged @luckyluke's change for detecting overflow of unsigned add, sub"Cristian Cadar
Will redo the merge to preserve original commits. This reverts commit a743d7072d9ccf11f96e3df45f25ad07da6ad9d6.
2015-02-10Merged @luckyluke's change for detecting overflow of unsigned add, subCristian Cadar
and mul operations. Refactored tests into two main cases, and disabled them on LLVM 2.9, which does not support -fsanitized=*signed-integer-overflow.
2014-09-19Removed code related to underConstrained, as it is unused (issue pointed out ↵Cristian Cadar
by @hpalikareva).
2014-09-13Add KLEE specific DEBUG macros.Daniel Dunbar
- This allows us to build in +Asserts mode even when LLVM isn't (by disabling the checks in that mode). - Eventually it would be nice to just move off of LLVM's DEBUG infrastructure entirely and just have our own copy, but this works for now. - Fixes #150.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-06-14 22:36:37 +0000