Changelog 22.2 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
###############################################################################
# Preliminary notes:                                                          #
# ------------------                                                          #
# Mark "-": change with an impact for users (and possibly developers).        #
# Mark "o": change with an impact for developers only.                        #
# Mark "+": change for Frama-C-commits audience (not in html version)         #
# Mark "*": bug fixed.                                                        #
# Mark "!": change that can break compatibility with existing development.    #
# '#nnn'   : BTS entry #nnn                                                   #
# '#!nnn'  : BTS private entry #nnn                                           #
Basile Desloges 's avatar
Basile Desloges committed
11
12
# '#@nnn'  : Gitlab frama-c/frama-c issue                                     #
# '##nnn'  : Gitlab pub/frama-c issue                                         #
13
14
15
16
# For compatibility with old change log formats:                              #
# '#?nnn'  : OLD-BTS entry #nnn                                               #
###############################################################################
# Categories:
17
18
19
20
21
#   E-ACSL      monitor generation
#   runtime     C runtime library (and memory model)
#   e-acsl-gcc  launcher e-acsl-gcc.sh
#   Makefile    Makefile
#   configure   configure
22
23
###############################################################################

Basile Desloges 's avatar
Basile Desloges committed
24
25
26
27
############################
Plugin E-ACSL <next-release>
############################

Basile Desloges 's avatar
Basile Desloges committed
28
29
-* runtime      [2021-03-30] Fix the end address of the memory segments in the
                RTL layouts.
Basile Desloges 's avatar
Basile Desloges committed
30
31
-  E-ACSL       [2021-03-25] Add support for `check` and `admit` annotations
                (frama-c/e-acsl#142).
Basile Desloges 's avatar
Basile Desloges committed
32
33
-* E-ACSL       [2021-03-25] Fix wrong computation of the base pointer when
                calling \valid predicate leading to undetected array overflows.
Basile Desloges 's avatar
Basile Desloges committed
34
35
36
37
38
39
40
41
42
43
44
45
-* E-ACSL       [2021-02-24] Fix crash when running another analysis after
                E-ACSL caused by E-ACSL breaking some internal kernel invariant
                (frama-c/e-acsl#145).
-  e-acsl-gcc   [2021-02-24] Try to find Frama-C binary in script or development
                directory if not present in PATH (frama-c/e-acsl#104).
-  e-acsl-gcc   [2021-02-24] Remove obsolete options from documentation and bash
                completion script (frama-c/e-acsl#104).
-  e-acsl-gcc   [2021-02-24] Deactivate Variadic translation when using
                incompatible option --validate-format-strings
                (frama-c/e-acsl#104).
-  e-acsl-gcc   [2021-02-24] Do not load Frama-C plugins when retrieving share
                and plugins paths (frama-c/e-acsl#104).
Basile Desloges 's avatar
Basile Desloges committed
46
47
-* runtime      [2021-02-18] Fix integration of contracts from the runtime
                library into Frama-C (#@999).
Basile Desloges 's avatar
Basile Desloges committed
48
49
-* E-ACSL       [2021-01-12] Fix crash when comparing two structs, which is
                currently unsupported (frama-c/e-acsl#139).
Julien Signoles's avatar
Julien Signoles committed
50
-* Makefile     [2021-01-05] Fix dependencies in bytecode-only compilation.
51
-  E-ACSL       [2020-12-09] Add RTL support for Windows.
Basile Desloges 's avatar
Basile Desloges committed
52
53
54
-  E-ACSL       [2020-11-17] Update e-acsl-gcc.sh so that the library dlmalloc
                can be compiled and used from sources.

55
56
57
58
#############################
Plugin E-ACSL 22.0 (Titanium)
#############################

59
-* E-ACSL       [2020-11-16] Fix soundness bug when checking
60
                initialization of a chunk of heap memory block.
61
62
-  E-ACSL       [2020-10-14] Add Support for Variadic generated functions in
                the AST (frama-c/e-acsl#128).
63
64
65
66
-  E-ACSL       [2020-10-06] Add support for the `\separated` predicate.
                (frama-c/e-acsl#31)
-* E-ACSL       [2020-10-06] Fix a soundness bug when translating a range with a
                logic variable.
67
68
-  E-ACSL       [2020-09-22] Support of complete and disjoint behavior
                (frama-c/e-acsl#92 and frama-c/e-acsl#27).
Basile Desloges 's avatar
Basile Desloges committed
69
70
-* runtime      [2020-09-15] Fix wrong value returned for the stack size in the
                segment memory model (frama-c/e-acsl#126).
Basile Desloges 's avatar
Basile Desloges committed
71
72
73
74
-  E-ACSL       [2020-09-15] Deprecate -e-acsl-full-mmodel in favor of
                -e-acsl-full-mtracking.
-  e-acsl-gcc   [2020-09-15] Deprecate --full-mmodel in favor of
                --full-mtracking.
75
-* E-ACSL       [2020-08-28] Fix crash that may occur when translating
76
77
                properties that have been proved valid by another plug-in
                (frama-c/e-acsl#106).
Julien Signoles's avatar
Julien Signoles committed
78
79
-! E-ACSL       [2020-08-28] Remove option -e-acsl-prepare-ast.
-! E-ACSL       [2020-08-28] Remove option -e-acsl-check.
80
81
82
83
84
85
-  E-ACSL       [2020-08-07] Add support for logical array comparison
                (frama-c/e-acsl#99).
-  E-ACSL       [2020-07-28] Add support of bitwise operators
                (frama-c/e-acsl#33).
-* E-ACSL       [2020-07-20] Fix unstable order of generated globals
                (frama-c/e-acsl#124).
Julien Signoles's avatar
Julien Signoles committed
86
-* E-ACSL       [2020-07-10] Fix translation of trange (incorrect length).
Basile Desloges 's avatar
Basile Desloges committed
87
88
-* E-ACSL       [2020-07-09] Decrease the number of allocated blocks when one
                block is freed.
Basile Desloges 's avatar
Basile Desloges committed
89
-  E-ACSL       [2020-06-19] Add support to create GMP rational from GMP
90
91
92
                integer (frama-c/e-acsl#120).
-* E-ACSL       [2020-06-18] Fix support of VLA memory tracking
                (frama-c/e-acsl#119).
Basile Desloges 's avatar
Basile Desloges committed
93

94
95
96
97
#############################
Plugin E-ACSL 21.0 (Scandium)
#############################

Basile Desloges 's avatar
Basile Desloges committed
98
99
-* E-ACSL       [2020-06-10] Fix ##13: bug when mixing integers and floats in
                annotations while -e-acsl-gmp-only is activated.
Basile Desloges 's avatar
Basile Desloges committed
100
101
-* E-ACSL       [2020-06-10] Fix a soundness bug (##14) when initializing
                rationals from integers.
102
-* E-ACSL       [2020-03-24] Fix automatic deactivation of plug-in Variadic when
Julien Signoles's avatar
Julien Signoles committed
103
                E-ACSL is directly called from Frama-C without using
104
                e-acsl-gcc.sh.
105
-  E-ACSL       [2020-03-10] Call E-ACSL's free functions for globals in a
106
                separate function at the end of main.
107
-  E-ACSL       [2020-03-10] Call `__e_acsl_memory_init` only if the memory
108
                model analysis is running.
109
-* E-ACSL       [2020-03-10] Fix frama-c/e-acsl#105 about misplaced
110
                `__e_acsl_delete_block` in presence of gotos to return statements.
111
-* E-ACSL       [2020-03-16] Fix #?1386 and frama-c/e-acsl#91 about the tracking
112
                of variables declared inside the body of switches.
113
114
-  E-ACSL       [2020-02-09] Improve verdict messages emitted by e_acsl_assert.
-* E-ACSL       [2020-01-06] Fix typing bug in presence of variable-length
115
                arrays that may lead to incorrect generated code.
116
-* E-ACSL       [2019-12-04] Fix bug with compiler built-ins.
117

118
119
120
121
############################
Plugin E-ACSL 20.0 (Calcium)
############################

122
123
-  E-ACSL       [2019-08-28] Support of rational numbers and operations.
-! E-ACSL       [2019-08-28] Deactivate the unsound support of real
124
125
                numbers (that are not rationals). They were previously
                unsoundly converted to floating point numbers.
Julien Signoles's avatar
Julien Signoles committed
126

Virgile Prevosto's avatar
Virgile Prevosto committed
127
128
129
130
##############################
Plugin E-ACSL 19.0 (Potassium)
##############################

131
-  E-ACSL       [2019-04-29] Support for logic functions and predicates
132
                without labels.
133
-  runtime      [2019-02-26] The behavior of __e_acsl_assert now depends on the
134
135
                runtime value of the global variable __e_acsl_sound_verdict:
                if 0, it means that its verdict is possibly incorrect.
136
-  E-ACSL       [2019-02-26] New option -e-acsl-instrument to instrument
137
138
                only a specified set of functions. It may lead to incorrect
                verdicts.
139
-  E-ACSL       [2019-02-19] New option -e-acsl-functions to monitor only
140
                annotations in a white list of functions.
141
-* runtime      [2019-02-04] Fix initialization of the E-ACSL runtime in
142
143
                presence of multiple calls to its initializer (for
                instance, if the main is a recursive function).
144
-* runtime      [2019-01-02] Fix overlap of TLS with other memory
Julien Signoles's avatar
Julien Signoles committed
145
                segments for large memory spaces.
146
-  E-ACSL       [2018-11-15] Predicates with empty quantifications
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
147
148
                directly generate \true or \false instead of nested loops.

149
150
151
152
##########################
Plugin E-ACSL 18.0 (Argon)
##########################

153
-* E-ACSL       [2018-11-13] Fix typing bug in quantifications when the
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
154
155
                guards of the quantifier variable cannot be represented into
                its type.
156
-* runtime      [2018-11-13] Fix bug #!2405 about memory initialization
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
157
                in presence of GCC constructors.
158
-* E-ACSL       [2018-10-23] Fix bug #2406 about monitoring of variables
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
159
                with incomplete types.
160
-* E-ACSL       [2018-10-04] Fix bug #2386 about incorrect typing when
161
                performing pointer subtraction.
162
-* E-ACSL       [2018-10-04] Support for \at on purely logic variables.
163
                Fix bug #1762 about out-of-scope variables when using \old.
164
-* E-ACSL       [2018-10-02] Fix bug #2305 about taking the address of a
165
                bitfield.
166
-  E-ACSL       [2018-09-18] Support for ranges in memory builtins
167
                (\valid, \initialized, etc).
Fonenantsoa Maurica 's avatar
Doc    
Fonenantsoa Maurica committed
168

169
170
171
######################################
Plugin E-ACSL 17.0 (Chlorine-20180501)
######################################
172

173
174
-  E-ACSL       [2018-03-30] Support for let binding.
-  E-ACSL       [2018-02-21] New option -e-acsl-replace-libc-functions to
175
176
                replace a few libc functions by built-ins that efficiently
                detects when they are incorrectly called.
177
-  E-ACSL       [2018-02-21] New option -e-acsl-validate-format-strings to
178
                detect format string errors in printf-like functions.
179
-* E-ACSL       [2018-02-21] Correct support of variable-length array
180
                (fix bug #1834).
181
182
-* runtime      [2018-02-16] Function __e_acsl_offset now returns size_t.
-* E-ACSL       [2018-02-07] Fix incorrect typing in presence of
183
184
185
                comparison operators (may only be visible when directly
                analyzing the E-ACSL's generated code with Frama-C without
                pretty-printing it).
186
-* runtime      [2018-01-30] E-ACSL aborted when run on a machine with a
187
                low hard limit on the stack size.
188
-* E-ACSL       [2018-01-08] Fix a crash when translating a postcondition
189
                that should generate a local variable (bts #2339).
190
-* e-acsl-gcc   [2017-11-28] Several files may be given to e-acsl-gcc.sh
Andre Maroneze's avatar
Andre Maroneze committed
191
                (as specified).
192
-* E-ACSL       [2017-11-27] Fix 'segmentation fault' of the generated monitor
193
                whenever the main has a precondition depending on the memory
Andre Maroneze's avatar
Andre Maroneze committed
194
                model.
195
-* E-ACSL       [2017-11-27] Restore behavior of option -e-acsl-valid broken
Andre Maroneze's avatar
Andre Maroneze committed
196
197
                since Phosphorus (included).

198
199
200
####################################
Plugin E-ACSL 16.0 (Sulfur-20171101)
####################################
Andre Maroneze's avatar
Andre Maroneze committed
201

202
-* E-ACSL       [2017-10-25] Fix bug #2303 about unnamed formals in
Andre Maroneze's avatar
Andre Maroneze committed
203
                annotated functions.
204
205
206
207
-  e-acsl-gcc   [2017-06-10] Add --free-valid-address option to e-acsl.gcc.sh.
-  e-acsl-gcc   [2017-05-29] Add --fail-with-code option to e-acsl.gcc.sh.
-  e-acsl-gcc   [2017-05-19] Add --temporal option to e-acsl.gcc.sh.
-  E-ACSL       [2017-05-19] New detection of temporal errors in E-ACSL
Andre Maroneze's avatar
Andre Maroneze committed
208
                through -e-acsl-temporal-validity (disabled by default).
209
210
211
-  e-acsl-gcc   [2017-03-26] Add --weak-validity option to e-acsl.gcc.sh.
-  e-acsl-gcc   [2017-03-26] Add --rt-verbose option to e-acsl.gcc.sh.
-  e-acsl-gcc   [2017-03-26] Add --keep-going option to e-acsl.gcc.sh allowing
Andre Maroneze's avatar
Andre Maroneze committed
212
                a program to continue execution after an assertion failure.
213
-  e-acsl-gcc   [2017-03-26] Add --stack-size and --heap-size options to
Andre Maroneze's avatar
Andre Maroneze committed
214
215
                e-acsl-gcc.sh allowing to change the default sizes of the
                respective shadow spaces.
216

217
########################################
218
Plugin E-ACSL 15.0 (Phosphorus-20170501)
219
########################################
220

221
-  runtime      [2017-03-29] The (much more efficient) shadow memory model is
222
                now used by default.
223
-* runtime      [2017-03-28] Fix backtrace when the failed instrumented programs
224
                do not require memory model.
225
226
-! e-acsl-gcc   [2017-03-19] Remove --print|-p option from e-acsl-gcc.sh
-  e-acsl-gcc   [2017-03-16] Add --check option to e-acsl-gcc.sh which allows
227
228
                to check the integrity of the generated AST before
                instrumentation.
229
230
-! e-acsl-gcc   [2017-03-03] Remove precond rte option from e-acsl-gss.sh.
-* E-ACSL       [2017-03-02] Fix bts #1740 about incorrect monitoring of
231
232
                memory properties when early exiting a block through
                goto, break or continue.
233
-* E-ACSL       [2017-03-01] Correct support of stdin, stdout and stderr
234
                in annotations.
235
-* E-ACSL       [2017-02-24] Fix crash with casts from non-integral terms to
236
                integral types (bts #2284).
237
-* E-ACSL       [2017-02-17] Fix bug with goto which points to a labeled
238
                statement which must be instrumented.
239
-* E-ACSL       [2017-01-23] Fix bug #2252 about pointer arithmetic with
240
                negative offsets.
241
-* E-ACSL       [2017-01-23] Fix bug with typing of unary and binary
242
243
                operations in a few cases: the generated code might have
                overflowed.
244

245
246
247
####################################
Plugin E-ACSL 0.8 (Silicon-20161101)
####################################
Julien Signoles's avatar
Julien Signoles committed
248

249
250
-* e-acsl-gcc   [2016-11-07] Added --rte-select feature to e-acsl-gcc.sh.
-* e-acsl-gcc   [2016-08-02] Added --rt-debug feature to e-acsl-gcc.sh.
251
                --enable-optimized-rtl configure option removed
252
253
-* configure    [2016-08-02] Added --enable-optimized-rtl option to configure
-* e-acsl-gcc   [2016-08-02] Removed --production|-P, --no-stdlib|-N and
254
                --debug-log|-D options of e-acsl-gcc.sh.
255
-* E-ACSL       [2016-07-21] Enable reporting of stack traces during assertion
256
                failures in instrumented programs.
257
-* e-acsl-gcc   [2016-07-13] Add an e-acsl-gcc.sh option (--print--models)
258
                allowing to print the names of the supported memory models.
259
-* E-ACSL       [2016-07-01] Add monitoring support for aligned memory
260
                allocation via posix_memalign and aligned alloc functions.
261
-* runtime      [2016-07-01] Add local version of GMP library customized for use
262
                with E-ACSL runtime library.
263
-* runtime      [2016-07-01] Add custom implementation of malloc for use with
264
                E-ACSL runtime library (via jemalloc library).
265
-  E-ACSL       [2016-05-31] New option -e-acsl-builtins which allows to
266
267
                declare pure C functions which can be used in logic
                function application.
268
-  E-ACSL       [2016-05-23] Re-implementation of the type system which
269
                improves the efficiency of the generated code over integers.
270
-* E-ACSL       [2016-05-23] Fix bug #2191 about complicate structs and
271
                literate string.
272
-* e-acsl-gcc   [2016-05-22] Add an e-acsl-gcc.sh option (--rte|-a) allowing to
273
274
                annotate the source program with memory-safety assertions prior
                to instrumentation.
275
276
277
278
279
-* E-ACSL       [2016-05-23] Fix bug #1395 about recursive functions.
-* Makefile     [2016-04-07] Fix 'make install' when executed within Frama-C.
-* runtime      [2016-03-31] Improve performance of Patricia Trie memory model.
-* Makefile     [2016-02-25] Fix 'make clean' in tests.
-* runtime      [2016-01-15] Fix several bugs related to incorrect partial
280
281
                initialization of tracked memory blocks in the E-ACSL
                memory model library.
282

283
284
285
######################################
Plugin E-ACSL 0.6 (Magnesium_20151002)
######################################
286

287
-* e-acsl-gcc   [2016-01-22] Add an e-acsl-gcc.sh option allowing to skip
288
                compilation of original sources.
289
290
-* Makefile     [2016-01-15] Fix installation with custom --prefix.
-* runtime      [2016-01-05] Fix bug in the memory model that caused the
291
                tracked size of heap memory be computed incorrectly.
292
-  e-acsl-gcc   [2015-12-15] Add a convenience script e-acsl-gcc.sh for
293
                small runs of the E-ACSL plugin.
294
-* E-ACSL       [2015-12-08] Fix bug #1817 about incorrect initialization of
295
                literal strings in global arrays with compound initializers.
296
-* runtime      [2015-11-06] Fix a crash occuring when using a recent libc
297
                while GMP headers provided by E-ACSL are used.
298

299
300
301
###################################
Plugin E-ACSL 0.5 (Sodium_20150201)
###################################
Julien Signoles's avatar
Julien Signoles committed
302

303
-  E-ACSL       [2015-06-01] Support of \freeable. Thus illegal calls to
304
                free (e.g. double free) are detected.
305
306
-* E-ACSL       [2015-05-28] Fix types of \block_length and \offset.
-  E-ACSL       [2015-05-27] Search .h in the E-ACSL memory model by
307
                default (easier to use declarations like __memory_size).
308
-  E-ACSL       [2015-05-27] Compatibility with new Frama-C Sodium option
309
                -frama-c-stdlib.
310
311
-* E-ACSL       [2015-04-28] Fix bug when using fopen.
-* E-ACSL       [2015-03-06] Fix bugs #1636 and #1837 about scoping of literal
312
                strings.
313
314
o  E-ACSL       [2014-12-17] Export a minimal API for other plug-ins.
-* E-ACSL       [2014-10-27] Add a missing cast when translating an integral
315
                type used in a floating point/real context in an annotation.
316

317
318
319
###################################
Plugin E-ACSL 0.4.1 (Neon_20140301)
###################################
Julien Signoles's avatar
Julien Signoles committed
320

321
322
323
324
325
-* E-ACSL       [2014-08-05] Fix bug #1838 about memset.
-* E-ACSL       [2014-08-05] Fix bug #1818 about initialization of globals.
-* E-ACSL       [2014-08-04] Fix bug #1696 by clarifying the manual.
-* E-ACSL       [2014-08-04] Fix bug #1831 about argc and argv.
-* E-ACSL       [2014-07-19] Fix bug #1836 about one-off error when
326
                computing the block which a pointer points to.
327
-* E-ACSL       [2014-07-08] Fix bug #1695 about using some part of the
328
                (Frama-C) libc which prevents linking of the generated C code.
329
-* E-ACSL       [2014-05-21] Fix bug #1782 about incorrect URL in the
330
                documentation.
331
-  E-ACSL       [2014-03-27] Remove spurious warnings when using type real
332
                numbers.
333
-* E-ACSL       [2014-03-26] Fix bug #1692 about wrong localisation of
334
                some messages.
335
-  E-ACSL       [2014-03-26] Remove a spurious warning when an annotated
336
                function is first declared, then defined.
337
-* E-ACSL       [2014-03-26] Fix bug #1717 about instrumentation of
338
                labeled statements.
339
340
-* E-ACSL       [2014-03-25] Fix bug #1716 with annotations in while(1).
-* E-ACSL       [2014-03-25] Fix bug #1715 about -e-acsl-full-mmodel which
341
                generates incorrect code.
342
-* E-ACSL       [2014-03-17] Fix bug #1700 about non-ISO empty struct.
Julien Signoles's avatar
Julien Signoles committed
343

344
345
346
#################################
Plugin E-ACSL 0.4 (Neon_20140301)
#################################
347

348
-* E-ACSL       [2014-01-28] Fix bug #1634 occuring in presence of static
349
                addresses.
350
-* E-ACSL       [2013-09-26] Fix incorrectness which may occur in presence
351
                of aliasing.
352
-* E-ACSL       [2013-09-25] Some loop invariants were tagged as "assertions".
353

354
355
356
#####################################
Plugin E-ACSL 0.3 (Fluorine_20130601)
#####################################
Julien Signoles's avatar
Julien Signoles committed
357

358
-  E-ACSL       [2013-09-18] More precise message for unsupported contract
359
                clauses.
360
361
362
363
364
-  E-ACSL       [2013-09-18] Use GMP still less often.
-* E-ACSL       [2013-09-18] Fix bug which may occur with divisions and modulos.
-  runtime      [2013-09-10] Improve ACSL contracts of the E-ACSL C library.
-  E-ACSL       [2013-09-06] Support of loop invariants.
-* E-ACSL       [2013-09-04] Fix bug when monitored global variables have
365
                initializers (bts #1478).
366
-* E-ACSL       [2013-09-04] Fix bug when mixing -e-acsl-prepare and
367
                running E-ACSL in another project (bts #!1473).
368
369
370
-* E-ACSL       [2013-06-26] Fix crash with typedef on pointer types.
-  E-ACSL       [2013-06-21] Fewer unknown locations.
-* E-ACSL       [2013-06-18] Fix bug when generating RTEs on the E-ACSL
371
                generated project.
372
-* E-ACSL       [2013-05-30] Fix -e-acsl-debug n, with n >= 2.
Julien Signoles's avatar
Julien Signoles committed
373

374
375
376
#####################################
Plugin E-ACSL 0.2 (Fluorine_20130401)
#####################################
Julien Signoles's avatar
Julien Signoles committed
377

378
-  E-ACSL       [2013-01-09] New option -e-acsl-valid. By default, valid
379
                annotation are not translated anymore.
380
-* E-ACSL       [2013-01-09] Fix bug when translating a postcondition of a
381
382
                function where the init state is the same than the final
                state (bts #!1300).
383
384
385
386
387
-  E-ACSL       [2013-01-09] Support of undefined function with a contract.
-  E-ACSL       [2012-12-20] Support of ghost variables and statements.
-* E-ACSL       [2012-12-13] Fix bug with complex term left-values.
-  E-ACSL       [2012-11-27] Support of \valid_read.
-  E-ACSL       [2012-11-27] Prevent runtime errors in annotations, except
388
                uninitialized variables.
389
-  E-ACSL       [2012-11-19] Support of floats in annotations. Approximate
390
                reals by floats.
391
392
393
394
395
396
397
-  E-ACSL       [2012-10-25] Support of \valid.
-  E-ACSL       [2012-10-25] Support of \initialized.
-  E-ACSL       [2012-10-25] Support of \block_length.
-  E-ACSL       [2012-10-25] Support of \offset.
-  E-ACSL       [2012-10-25] Support of \base_addr.
-* E-ACSL       [2012-09-13] Fix bug with very long ACSL integer constants.
-  E-ACSL       [2012-06-27] Continue to convert the other pre/post-conditions
398
                even if one fails.
399
400
-  runtime      [2012-04-27] Improve ACSL spec of E-ACSL' C library.
-* Makefile     [2012-01-27] Fix compilation bug when configuring with
401
                --enable-external.
402
403
404
405
406
407
-  E-ACSL       [2012-01-25] Nicer generated variable names.
-* E-ACSL       [2012-01-24] Fix bug with lazy operators in term position.
-* E-ACSL       [2012-01-24] Fix bug with boolean.
-* E-ACSL       [2012-01-24] Fix bug with negation and GMP integers.
-* E-ACSL       [2012-01-24] Fix bug with conditional and GMP integers.
-  runtime      [2012-01-24] Function e_acsl_assert now consistent with
408
                standard assert.
409
410
-  E-ACSL       [2012-01-23] Support of bitwise complementation.
-  E-ACSL       [2012-01-20] Use GMP arithmetics only when required
411
                (i.e. mostly never in practice).
Julien Signoles's avatar
Julien Signoles committed
412

413
414
415
#####################################
Plugin E-ACSL 0.1 (Nitrogen_20111001)
#####################################
416

417
-  E-ACSL       [2012-01-06] First public release.
418
419

###################################