about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2019-02-24 21:51:54 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2019-03-19 16:49:16 +0000
commit2634250dd3bd7aae225a80e4f024874752432752 (patch)
tree65c0df1ccb1d188a47d679fe6505cdade6f0dc9b
parent265c25c6120205a9949928aa570ac9644011c0ca (diff)
downloadklee-2634250dd3bd7aae225a80e4f024874752432752.tar.gz
Release notes for 2.0 v2.0
-rw-r--r--NEWS93
1 files changed, 93 insertions, 0 deletions
diff --git a/NEWS b/NEWS
index 32d5c59a..b50fef77 100644
--- a/NEWS
+++ b/NEWS
@@ -1,3 +1,96 @@
+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)