[klee-dev] KLEE 1.3.0 released
Cristian Cadar
c.cadar at imperial.ac.uk
Wed Nov 30 18:10:52 GMT 2016
KLEE 1.3.0 is now available at
https://github.com/klee/klee/releases/tag/v1.3.0.
A key change is a more deterministic behavior of KLEE, which is
essential for KLEE-related experiments, thanks primarily to Martin
Nowack's work. KLEE-Web, announced last month, has also been made
available since we last released KLEE at http://klee.doc.ic.ac.uk/. The
release also adds several other new features, some option renames, bug
fixes and improved documentation, which are all detailed in the release
notes below.
Thanks for everyone's contributions!
Cristian
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)
More information about the klee-dev
mailing list