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)