KLEE 3.1, 29 February 2024 ========================== Incorporating changes from 8 June 2023 to 29 February 2029. Maintainers during this time span: @ccadar, @MartinNowack, @251. Documentation at http://klee.github.io/releases/docs/v3.1 == Major features == - KDAlloc is now the default allocator in KLEE (KDAlloc was introduced in KLEE 3.0) - New execution tree implementation and klee-exec-tree tool (@251) - Resolve memory reads/writes to single objects in more cases (@tkuchta) - Concretize values based on seeds when available (@ccadar) == LLVM support == - Current recommended version is still LLVM 13 - Added support for LLVM 15 and 16 (@MartinNowack) - Removed support for LLVM <11 (@danielschemmel) - KLEE 3.1 will be the last version with support for LLVM <13 == Options, scripts and KLEE intrinsics added, changed or removed == - New klee-exec-tree tool (@251) - New --write-exec-tree and --exec-tree-batch-size options (@251) - Renamed --compress-process-tree to --compress-exec-tree (@ccadar) - PTree is now called ExecutionTree in the code (@ccadar) - KDAlloc (--kdalloc) is now enabled by default (@ccadar) - Replaced --suppress-external-warnings and --all-external-warnings with --external-call-warnings=none|once-per-function|all (@ccadar) - Keep in the KLEE and Kleaver help menus only the KLEE/Kleaver option categories (@ccadar) - Removed --cex-cache-exp, a broken experimental optimisation for validity (@ccadar) - Removed --zero-seed-extension, and merge it with --allow-seed-extension (@ccadar) == Other changes == - Fixed some interactions with external code (@ccadar, mishok2503) - Improvements to KDAlloc (@danielschemmel) - Avoid generating array names in solver builders that could accidently collide (@MartinNowack) - Function has_permission in the POSIX model now returns permission error a single time in symbolic execution mode (@ccadar) - Smaller refactorings, fixes and improvements, test cases, maintenance, comments, web version, website, etc. (@251, @ccadar, @dependabot, @danielschemmel, @davidtr1037, @jbuening, @marco6, @MartinNowack, @McSinyx, @sp1ff) KLEE 3.0, 7 June 2023 ===================== Incorporating changes from 8 April 2022 to 7 June 2023. Maintainers during this time span: @ccadar, @MartinNowack, @251. (@251 joined as a new maintainer during 2022). Documentation at http://klee.github.io/releases/docs/v3.0 == Major features == - Added support for the KDAlloc memory allocator, which enables KLEE to more robustly detect use-after-free errors, improves the detection of buffer overflows, and provides deterministic memory allocation (@danielschemmel, based on https://srg.doc.ic.ac.uk/publications/22-kdalloc-ecoop.html) - Enabled KLEE to support UBSan-added checks (@operasfantom) - Added support for concrete inline assembly, which is now handled as an external call (@mishok2503) == LLVM support == - Current recommended version is LLVM 13 - Added support for LLVM 14 (@lzaoral) - Removed support for LLVM <9 - KLEE 3.0 will be the last version with support for LLVM <11 == Options, scripts and KLEE intrinsics added, changed or removed == - Renamed gen-bout to ktest-gen, and gen-random-bout to ktest-randgen (@ccadar) - Added option --stp-sat-solver for selecting the SAT solver used by STP (@251) - Added many more runtime statistics that can be inspected with klee-stats, and renamed several of them (@251) - Removed unused model_version from the tests generated when the POSIX runtime is enabled (@ccadar) - Removed unused option --replay-keep-symbolic (@251) - Added support for the @llvm.f{ma,muladd}.f* intrinsics (@lzaoral) - Allow UcLibc to support a runtime option rather than a compile-time one (@arrowd) - Added support for llvm.experimental.noalias.scope.decl (@operasfantom) - Modified names of SMT variables to use underscores instead of dashes, e.g., A_data instead of A-data (@ccadar) == Other changes == - Overhaul of KLEE's CI and build scripts (@MartinNowack, @jbuening) - Introduce separate categories for different kinds of undefined behavior (@operasfantom) - Support arguments of width 128, 256 and 512 bits for external calls (@operasfantom) - Added check for nonnull path APIs in fstatat (@251, @jbuening) - Fixed a bug in KLEE libc's implementation of strcmp, where characters were not compared as unsigned (@ccadar) - Added support for Differential ShellCheck (@jamacku) - Fixed a bug triggered when --entry-point and --libc=uclibc are used together (@ccadar) - Fixed a bug with --use-batching-search ignoring disabled time budget (@jbuening) - Smaller refactorings, fixes and improvements, test cases, maintenance, comments, web version, website, etc. (@251, @andronat, @arrowd, @ccadar, @danielschemmel, @dependabot, @fwc, @jamesjer, @jbuening, @jryans, @kt218, @lzaoral, @m-davis, @MartinNowack, @McSinyx, @mishok2503, @operasfantom, @prncoprs, @rriley, @rshariffdeen, @sava-cska, @ZHYfeng) KLEE 2.3, 4 April 2022 ====================== Incorporating changes from 8 December 2020 to 4 April 2022. Maintainers during this time span: @ccadar and @MartinNowack Documentation at http://klee.github.io/releases/docs/v2.3 == LLVM support == - Current recommended version is LLVM 11 - Added support for LLVM 12 and 13 (@lzaoral) - Removed support for LLVM <6 - KLEE 2.3 will be the last version with support for LLVM <9 == Options, scripts and KLEE intrinsics added, changed or removed == - Added --max-static-pct-check-delay to specify the number of forks after which the --max-static-*-pct checks are enforced (@ccadar) - In klee-stats, added --print-columns to print user-defined columns, e.g. --print-columns 'Path,Instrs,Time(s)' (@251) - Disabled Doxygen generation by default; it can be enabled via CMake option ENABLE_DOXYGEN=ON == Other changes == - Introduced termination categories and branch types (@251) - Added support for more recent versions of Google Test (@jbuening) - Fixed --prefer-cex, which was crashing in some cases (@TarasBereznyak) - Added support for executing 32bit code, with some limitations (@lzaoral) - Improved exception handling (@jbuening) - Various improvements to klee-stats (@251) - Fixed UBSan reporting in the CI and fixed several errors reported by UBSan (@lzaoral) - Fixed path statistics with -dump-states-on-halt=false (@251) - Differentiate between partial and completed paths in the summary printed at the end (@251) - Improved determinism (@jbuening) - Added support for LLVM abs (except for the vector variants), llvm.roundeven and llvm.{s,u}{max,min} intrinsics (@lzaoral) - Fixed and improved model for getcwd (@251) - Fixed a silent concretization case in Executor::fork (@ccadar) - Added a large number of KLEE-related publications to the website (@251) - Fixed the memory usage computation on macOS (@ccadar) - Removed or updated obsolete Doxygen options and added Doxygen generation to the CI (@ccadar) - Smaller refactorings, fixes and improvements, test cases, maintenance, comments, web version, website, etc. (@251, @aesophor, @arrowd, @bathooman, @ccadar, @carlocab, @davidtr1037, @dependabot, @futile, @iangneal, @jbuening, @jirislaby, @jiseongg, @jordr, @lzaoral, @MartinNowack, @numinit, @operasfantom, @prncoprs) KLEE 2.2, 7 December 2020 ========================= Incorporating changes from 4 March 2020 to 7 December 2020. Maintainers during this time span: @ccadar and @MartinNowack Documentation at http://klee.github.io/releases/docs/v2.2 == Major features == - Added support for C++ exceptions (@corrodedHash, @futile, @jbuening) - Correctly copy variadic arguments with byval attribute (@ccadar) - Modified the random path searcher to work on a subset of states (@kren1) - Added state IDs to improve determinism (@251) - Overhauled the (Travis CI) build scripts (@MartinNowack) - Restructured header files (@ccadar) == LLVM support == - Current recommended version is LLVM 9 - Added support for LLVM 11 (@lzaoral) - We have decided to extend support for LLVM 3.8 to 5, but KLEE 2.2 will be the last version with support for LLVM <6 == Options, scripts and KLEE intrinsics added, changed or removed == - Changed --debug-print-instructions to also print state IDs (@251) - Added -rng-initial-seed to set the seed for KLEE's random number generator (@251) - Added klee_is_replay intrinsic which returns whether the code is being executed symbolically or in replay mode (@alastairreid) - Added --compress-process-tree to remove intermediate nodes in the process tree when possible (@sebastianpoeplau) - Added klee-zesti, a ZESTI-like wrapper (@kren1) - Added --table-format=readable-csv/csv to klee-stats (@251) == Other changes == - Fixed GlobalAlias initialization (@jbuening) - Enforced fork/branch limits in branch() and fix double termination (@251) - Enhanced POSIX runtime in the case where a symbolic file is given as an absolute path, i.e. /current/work/dir/A (@kren1) - Named jobs in Travis CI for better visualization of results (@ccadar) - Fixes and improvements in the statistics code including klee-stats (@251) - Added a simple model for GET/SET_LK (@kren1) - Fixed bug in the handling of vectorized code (@Warfley) - Fixed bug in the handling of STP array names (@MartinNowack) - Fixed bug in Z3Solver::getConstraintLog (@daniel-grumberg) - Added support for reading strings from the middle of objects in readStringAtAddress (@mchalupa) - Disabled asm lifting for memory fences with return values (@MartinNowack) - Fixed bug when the search requires MD2U (@adrianherrera) - Added support for fshr/fshl intrinsics (@alastairreid) - Refactored the constraint manager (@MartinNowack) - Changed DiscretePDF to use IDs instead of pointers to remove nondeterminism (@251) - Added a more robust handling of unknown intrinsics: if an unknown intrinsic is encountered on a path, that path is terminated but the others can proceed (@alastairreid) - Fixed PTree::remove to clean the tree properly (@sebastianpoeplau) - Added support for multiple symbolic files to gen-bout (@kren1) - Added a PR template, with a checklist documenting the most frequent issues we have encountered (@ccadar) - Fixed the behaviour of klee-stats for broken or empty DBs (@251) - Added support for klee_open_merge and klee_close_merge in replay (@ccadar) - Fixed the handling of global variables while validating direct call targets (@MartinNowack) - Fixed the handling of the fabs intrinsic (@dlaprell) - Added support for the fneg instruction (@jbuening) - Removed incompatibility between merging and the random path search (@251) - Fixed the behaviour of klee-libc to call the functions in __cxa_atexit in reverse order (@tomsik68) - Fixed the behaviour of bcmp in klee-libc (@alastairreid) - Added support for multi-version bitcode libraries (@MartinNowack) - Added support for several fortified functions, -D_FORTIFY_SOURCE (@ccadar) - Modernize ref<> and isa<> nullptr checks (@jbuening) - Switched CI from Travis CI to GitHub Actions (@MartinNowack, with thanks to @jordr) - Smaller refactorings, fixes and improvements, test cases, maintenance, comments, web version, website, etc. (@251, @adrianherrera, @alastairreid, @andrewvaughanj, @andronat, @arrowd, @ccadar, @dependabot, @i-ky, @jbuening, @jiseongg, @jordr, @kren1, @lahiri-phdworks, @MartinNowack, @yxliang01) KLEE 2.1, 3 March 2020 ======================= Incorporating changes from 20 March 2019 to 3 March 2020. Maintainers during this time span: @ccadar and @MartinNowack Documentation at http://klee.github.io/releases/docs/v2.1 == Major features == - New container-based architecture for KLEE Web (@Denis-Gavrielov, @andronat) - Changed the statistics framework to use SQL and improve klee-stats (@kren1, @251) - Added Grafana visualisation to klee-stats (@gdish, @KennyMacheka, @kren1) - Brought gen-random-bout up-to-date (@domainexpert) - Fixed support for FreeBSD (@arrowd) - Replaced signalling with synchronous checks for implementing timers (@251) - Improved reference handling (ref<>) (@MartinNowack) == LLVM support == - Added support for LLVM 9 and 10 (@jbuening) - Removed support for LLVM <3.8 (@jbuening) - KLEE 2.1 will be the last version with support for LLVM <6 == Options, scripts and KLEE intrinsics added, changed or removed == - Replaced intrinsic klee_alias_function("foo", "bar") with option -function-alias=foo:bar, which supports regular expressions (@jbuening, @SolalPirelli) - Removed -max-instruction-time (@251) - Added -timer-interval (default 1s) to specify the minimum interval to check timers (@251) - Added nurs:rp searcher which uses non-uniform random search with 1/2^depth (@kren1) - Replaced the behavior of the nurs:depth searcher to use NURS with depth (@kren1) - klee-stats: new --grafana option (see above) - klee-stats: new --to-csv option for converting statistics to the CSV format (@251) - klee-stats: removed --sample-interval, --sort-by, --compare-by, --precision. These can be now simulated by querying the SQL database directly (@kren1) - klee-replay: added --keep-replay-dir option to keep the replay directory (@ccadar) == Other changes == - Added support for llvm.fabs (@futile) - Added support for saturated arithmetic intrinsics (@mateon1) - Added support for llvm.objectsize (@MartinNowack) - Added support for llvm.is.constant (@arrowd) - Fixed bugs in --optimize-array (@kren1) - Removed statistics limit from istats (@MartinNowack) - Refactored PTree (@251) - Improved klee-replay and made it safe to run multiple instances in parallel (@ccadar) - Check if read-only objects are marked as symbolic (@MartinNowack) - Allow main() with 3 arguments (@ccadar) - Improved the structure of the codebase (@ccadar) - Improved KLEE's CI build scripts (@MartinNowack, @jbuening) - Smaller refactorings, fixes and improvements, test cases, maintenance, comments, web version, website, etc. (@251, @arrowd, @benquike, @ccadar, @cyberwookiee, @danielschemmel, @Denis-Gavrielov, @dependabot, @domainexpert, @futile, @gdish, @JasonPap, @jbuening, @jirislaby, @KennyMacheka, @kren1, @MartinNowack, @qurben) KLEE 2.0, 19 March 2019 ======================== Incorporating changes from 22 July 2017 to 19 March 2019 Maintainers during this time span: @AndreaMattavelli, @ccadar, @delcypher, @MartinNowack Documentation at http://klee.github.io/releases/docs/v2.0 == Major features == - Added support for KLEE array optimizations from ISSTA'17 paper "Accelerating Array Constraints in Symbolic Execution" (@AndreaMattavelli, @MartinNowack, @ccadar) - Added support for LibC++ (--libcxx flag) (@corrodedHash, @futile, @MartinNowack) - Added support for CVC4 and Yices2 via metaSMT (@hoangmle) - Added better path merging functionality via klee_open_merge and klee_close_merge (@corrodedHash, @futile) - Fixed support for vector instructions (@MartinNowack) - Support for recent LLVM versions (see "LLVM support" below) - New categorized --help menu, with LLVM options hidden by default (see "Options, scripts and intrinsics changed or removed" below) == LLVM support == - Added support for LLVM 3.7 - 7.0 (@jirislaby) - Added support for LLVM 8.0 (@MartinNowack) - KLEE 2.0 will be the last release with support for LLVM 3.4 to 3.7 - Removed support for LLVM <3.4 (@MartinNowack) == Options, scripts and intrinsics changed or removed == - Renamed several options (@ccadar) * --environ to --env-file * --no-output to --write-no-tests * --red-zone-space to --redzone-size * --run-in to --run-in-dir * --seed-out to --seed-file * --seed-out-dir to --seed-dir * --stop-after-n-tests to --max-tests * --use-cache to --use-branch-cache * --use-construct-hash to --use-construct-hash-stp * --warn-all-externals to --warn-all-external-symbols - Replaced --no-externals and --allow-external-sym-calls with --external-calls (@ccadar) - Added --libcxx option to enable LibC++ support (see "Major features" above) - Added option --max-stack-frames to limit the number of stack frames used (@MartinNowack) - Added --klee-call-optimisation option, which can be set to false to disable some optimizations that interact incorrectly with the checks injected by KLEE. See https://github.com/klee/klee/pull/1059 for more details (@MartinNowack) - Added support for disabling --batch-instructions and --batch-time by setting them to zero (@ccadar) - Removed option --disable-opt (@ccadar) - Removed klee-gcc and klee-clang (@251, @MartinNowack) - Removed support for klee_make_symbolic with two arguments (@ccadar) - Allow NULL as name to klee_int, to create "unnamed" object (@251) - New time API used in options (@251) - Improved the output of ktest-tool and added an --extract option (@251) - Categorized options in --help, improved help messages, and hid LLVM options by default (@ccadar) == Other changes == - Updated build system to detect whether STP, Z3, metaSMT are available (@delcypher) - Fixed test case counter: previously the number of test cases generated by KLEE was always incremented, even if a symbolic solution was not found (@andreamattavelli) - Added checks for div/mod by zero and overshifts in constant expressions (@ccadar) - Fixed a bug causing KLEE to generate files with no permissions bits set (@ccadar) - Added clean_doxygen target and a global clean_all target to the build system (@delcypher) - Fixed initialization of distance to uncovered instructions when KLEE relies on default searchers (@andreamattavelli) - Fixed assert in BFSSearcher that does not hold as part of interleaved searcher (@jbuening) - Fixed huge allocation size constant (@davidtr1037) - Added Codecov support (@andreamattavelli, @MartinNowack) - Store cex cache stats and report them in klee-stats (@helicopter88) - Fixed incorrectly incremented stats for dumped states (@251) - Fixed bug where KLEE would not output test cases when --exit-on-error is enabled (@buszk) - Added support for blockaddress and indirectbr instructions (@251) - Implemented klee_prefer_cex() and klee_abort() for replay mode (@Lysxia) - Fixed handling of errno when external functions are invoked (@MartinNowack) - Fixed utimes() behavior for symbolic files when the second argument is NULL (@yxliang01) - Improved handling of constant array in Z3 (@kren1) - Improved the handling of external calls with symbolic data (@kren1) - Abort execution if --only-output-states-covering-new is enabled but its dependency --output-istats is not (@ccadar) - Improved ConstantExpr performance (@kren1) - Improved linking and optimizations order (@MartinNowack) - Enabled TCMalloc by default (@kren1) - Disabled unit testing in default build (@AndreaMattavelli) - Added resolve time to klee-stats --print-all (@251) - Improved the startup sequence enabling the POSIX runtime (@MartinNowack) - Added ASan and UBSan flags to lit (@251) - Added support for handling multiple SIGSEGVs in external calls (@251) - Added checks for correct usage of the POSIX mode (@ccadar) - Added support for klee-replay on OSX (@251) - Added lowering pass for atomic instructions (@erzett, @futile) - Improved handling of metadata (@MartinNowack) - Improved efficiency of div/mod and shift checks by skipping unnecessary checks (@MartinNowack) - Added support for memalign (@corrodedHash) - Enable C++14 support (@MartinNowack) - Fixed issue with aliases that point to other aliases (@jbuening) - Added workaround for the LLVM bug PR39177 (@jbuening) - Updated dependency build system for KLEE (@MartinNowack) - Fixed the Docker deployment for KLEE (@MartinNowack) - Added support for compiling KLEE with MSan and UBSan's integer sanitizer (@MartinNowack) - Fixed representation of ReadExpr's into equivalent arrays (@MartinNowack) - Added support for debug information provided by newer LLVM versions (@MartinNowack) - Added many KLEE-related publications (@251) - Smaller refactorings, fixes and improvements, test cases, maintenance, comments, web version, website, etc. (@andronat, @251, @andreamattavelli, @ccadar, @corrodedHash, @danielschemmel, @delcypher, @itbot08, @jasondavies, @jbuening, @jirislaby, @kren1, @Lysxia, @MartinNowack, @Mic92, @odeits-vidder, @SolalPirelli, @szeyiuchau, @Tipwheal, @yannicnoller) KLEE 1.4.0, 21 July 2017 ======================== (Incorporating changes from 4 November 2016 up to and including 21 July 2017) Documentation at http://klee.github.io/releases/docs/v1.4.0/ This will be the last version supporting LLVM 2.9 and the autoconf build system. - New CMake build system (@delcypher, @jirislaby) - Added support for vectorized instructions (@delcypher) - Fixed and documents BFS searcher behaviour (@MartinNowack, @ccadar) - Renames .pc files to .kquery files (@holycrap872) - Removed option --randomize-fork (@ccadar) - Changed preferred permissions from 0622 to the more standard 0644 in the POSIX model (@ccadar) - New target name, "make systemtests", for running the system tests. This replaces "make test". Running the unit tests is still accomplished via "make unittests". - Better support for MacOS (@andreamattavelli, @delcypher) - Enabled support for ASan builds of KLEE (@delcypher) - Support long long values in --stop-after-n-instructions for LLVM > 2.9 (@andreamattavelli) - Teach KLEE to respect the requested memory alignment of globals and stack variables when possible (@delcypher) - Added new option --warnings-only-to-file which causes warnings to be written to warnings.txt only (@ccadar) - metaSMT improvements (@hoangmle) - KLEE-web improvements (@andronat, @helicopter88) - Fixed bug in the implementation of NotExpr (@delcypher) - Fixed a bug leading to data loss when writing into files (@ccadar, @gladtbx) - Some improvements and refactoring to the Expr library (@delcypher) - Added missing constant folding opportunity when handling constant arrays (@andreamattavelli, @delcypher) - Teach klee::getDirectCallTarget() to resolve weak aliases (@delcypher) - Fixed handling of internal forks (@gladtbx) - Improved replay using libkleeRuntest (@delcypher) - Added -debug-assignment-validating-solver feature to check the correctness of generated assignments (@delcypher) - Added -debug-z3-dump-queries, -debug-z3-validate-models and -debug-z3-verbosity options useful for debugging the interaction with Z3 (@delcypher) - Added geq/lt-llvm- configs in lit (@jirislaby) - Work on supporting newer LLVM versions (@jirislaby) - Fixed bug where stats would not be updated on early exit (@delcypher) - Reworked the external dispatching mechanism (@delcypher) - Added support for creating release documentation (@delcypher) - Smaller refactorings, fixes and improvements, test cases, maintenance, comments, website, etc. (@adrianherrera, @akshaynagpal, @AlexxNica, @andreamattavelli, @bananaappletw, @bigelephant29, @bunseokbot, @ccadar, @delcypher, @emlai, @hoangmle, @jirislaby, @kren1, @levex, @Manouchehri, @MartinNowack, @mechtaev, @Mic92, @omeranson, @rtrembecky, @thestr4ng3r, @tomek-kuchta) KLEE 1.3.0, 30 November 2016 ============================ (Incorporating changes from 1 April up to and including 3 November 2016) * Improved determinism of KLEE, an essential feature for experiments involving KLEE (@MartinNowack) * KLEE-web has been improved and refactored, and now available at http://klee.doc.ic.ac.uk/ (@giacomoguerci, @helicopter88, @andronat, @ccadar, based on work by @ains, @ben-chin, @ilovepjs, @JamesDavidCarr, Kaho Sato, Conrad Watt, @ccadar) * Renamed --replay-out to --replay-ktest and --replay-out-dir to replay-ktest-dir (@delcypher) * Split creation of symbolic files and stdin in two distinct options, documented at http://klee.github.io/docs/options/#symbolic-environment (@andreamattavelli) * Support for logging queries before invoking the solver via --log-partial-queries-early, useful for debugging solver crashes (@MartinNowack) * Added --stats-write-after-instructions and --istats-write-after-instructions to update each statistic after n steps (@MartinNowack) * Added --compress-log and --debug-compress-instructions to gzip-compress logs (@MartinNowack) * Added --exit-on-error-type option for stopping execution when certain error types are encountered (@jirislaby) * Updated and improved metaSMT support and added TravisCI targets (@hoangmle) * Added option --debug-crosscheck-core-solver to allow crosschecking of solvers (@delcypher) * Explicitly made division total in STP (@ccadar) * Extended support for assembler raising (@MartinNowack) * Disabled --solver-optimize-divides, as the optimization is currently buggy (@ccadar) * Improved --debug-print-instructions options with more logging options (@andreamattavelli) * Improved stub for times() not to trigger a NULL dereference (@ccadar) * Allow relocation of installed KLEE tree (@ShayDamir) * Fixed bug in independent solver (@delcypher) * Fixed alignement of varargs (@MartinNowack) * Fixed variable shifting behavior with different sizes and generation of STP shift operations with variable amounts (@MartinNowack) * Fixed handling of non-sized globals (@jirislaby) * Fixed klee_get_obj_size() crash on 64-bit (@hutoTUM) * Fixed bug in Kleaver's parser (@andreamattavelli) * Refactorings, small fixes and improvements, test cases, maintenance and website: (@andreamattavelli, @ccadar, @delcypher, @domainexpert, @giacomoguerci, @hoangmle, @helicopter88, @jirislaby, @Justme0, @kren1, @MartinNowack, @mchalupa) KLEE 1.2.0, 31 March 2016 ========================= * Added native support for Z3 (@delcypher) * Made it possible to build KLEE without using STP and only MetaSMT (@delcypher) * Added support for tcmalloc, which allows KLEE to better track memory consumption (@MartinNowack) * Added support for lowering the ``llvm.objectsize`` intrinsic (@delcypher) * Added soname for Runtest dynamic library (@MartinNowack) * Added support to load libraries from command line (@omeranson) * Added command line flag --silent-klee-assume to suppress errors due to infeasible assumptions (Valentin Wüstholz, @wuestholz) * Changed code to print out arrays deterministically (@MartinNowack) * Improved klee-clang script (@msoos) * Added code to dump queries and assignments (@MartinNowack) * Code cleanup and refactorings (@delcypher, @MartinNowack) * Improvements to code infrastructure (@delcypher, @domainexpert, @MartinNowack, @mdimjasevic, @msoos) * Fixed several memory leaks (@delcypher) * Fixed a bug with how non-power of 2 values were written to memory (@kren1) * Fixed valueIsOnlyCalled() used by MD2U (@yotann) * Fixed SELinux signatures (@lszekeres) * Fixed incorrect position of Not in Expr::Kind (@delcypher) * Fixed wrong std::vector usage after reserve() call (@pollnossa) * Improved documentation (@bananaappletw, @ccadar, @delcypher, @mdimjasevic, @Teemperor, @ward, @wuestholz) KLEE 1.1.0, 13 November 2015 ============================ * Made LLVM 3.4 and STP 2.1.0 the recommended versions for installing KLEE (Cristian Cadar, @ccadar; Dan Liew, @delcypher; Martin Nowack, @MartinNowack; Mate Soos, @msoos) * Added instructions for using the Docker images (Dan Liew, @delcypher) * Added NEWS file to keep track of changes for each release (Cristian Cadar, @ccadar) * Added coverage information for the current KLEE codebase (Timotej Kapus, @kren1) * Added -entry-point=FOO option, where FOO is the name of the function to use as the entry point for execution (Riccardo Schirone, @ret2libc) * Switched STP to v2.1.0 (instead of the old r940) in TravisCI (Martin Nowack, @MartinNowack) * Improved Dockerfiles to use specific dependency versions (Dan Liew, @delcypher) * Bug fix: Fixed signed division by constant 1/-1 (Martin Nowack, @MartinNowack, reported by Timotej Kapus, @kren1) * Bug fix: Generate SRrem expressions correctly (Martin Nowack, @MartinNowack, reported by Timotej Kapus, @kren1) * Bug fix: Allowed the generation of initial values for queries with empty constraint set (Martin Nowack, @MartinNowack) * Bug fix: Fixed assertion failure in getDirectCallTarget (Sean Bartell, @yotann) * Bug fix/test improvement: Use a temporary directory instead of /tmp in futimesat test (Andrew Chi, @andrewchi) * Various fixes and improvements to the website (Eric Rizzi, @holycrap872; Martin Nowack, @MartinNowack; Bheesham Persaud, @bheesham; Gu Zhengxiong, @NoviceLive; Cristian Cadar, @ccadar) KLEE 1.0.0, 10 August 2015 ========================== # Recent changes (from 2015) * Several performance improvements to the counterexample cache, including changing some default behaviour (Eric Rizzi, @holycrap872) * Computing coverage of KLEE code in Travis CI (Timotej Kapus, @kren1) * Added an option --readable-posix-inputs which is used to turn on/off the CEX preferences added in the POSIX model (Eric Rizzi, @holycrap872; Cristian Cadar, @ccadar) * Lots of improvements to the build process (Dan Liew, @delcypher) * Added klee-clang as alternative to klee-gcc (Martin Nowack, @MartinNowack) * Added Dockerfile for building a KLEE Docker image (Dan Liew, @delcypher) * Added a new option, --rewrite-equalities, which makes it possible to disable the optimisation that rewrites existing constraints when an equality with a constant is added (Cristian Cadar, @ccadar) * Cleaner, more efficient timestamps (Emil Rakadjiev, @erakadjiev) * Improved integer overflow detection (Luca Dariz, @luckyluke)