diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-02-24 21:51:54 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-03-19 16:49:16 +0000 |
commit | 2634250dd3bd7aae225a80e4f024874752432752 (patch) | |
tree | 65c0df1ccb1d188a47d679fe6505cdade6f0dc9b | |
parent | 265c25c6120205a9949928aa570ac9644011c0ca (diff) | |
download | klee-2634250dd3bd7aae225a80e4f024874752432752.tar.gz |
Release notes for 2.0 v2.0
-rw-r--r-- | NEWS | 93 |
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) |