forked from klee/klee
-
Notifications
You must be signed in to change notification settings - Fork 0
/
NEWS
136 lines (121 loc) · 8.87 KB
/
NEWS
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
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)