path: root/NEWS

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)