KLEE 3.1, 29 February 2024

Incorporating changes from 8 June 2023 to 29 February 2024.
Maintainers during this time span: @ccadar, @MartinNowack, @251.
Documentation at http://klee.github.io/releases/docs/v3.1

Major features and important changes

• New execution tree implementation and klee-exec-tree tool (@251)
• KDAlloc is now the default allocator in KLEE (KDAlloc was introduced in KLEE 3.0)
• Resolve memory reads/writes to single objects in more cases (@tkuchta)
• Concretize values based on seeds when available (@ccadar)
• Fixed some interactions with external code (@ccadar, @MartinNowack, mishok2503)

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

• 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 March 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 on 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)

First official release for KLEE.

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)