diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 3b8b97a86519718bc8a7591c60b1ed853a889e12..e535d9b3fb164675e63ccd7e2d15aa9c6b36be93 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -12,11 +12,11 @@
# '#?nnn' : OLD-BTS entry #nnn #
###############################################################################
# Categories:
-# E-ACSL monitor generation
-# runtime C runtime library (and memory model)
-# e-acsl-gcc launcher e-acsl-gcc.sh
-# Makefile Makefile
-# configure configure
+# E-ACSL monitor generation
+# runtime C runtime library (and memory model)
+# e-acsl-gcc launcher e-acsl-gcc.sh
+# Makefile Makefile
+# configure configure
###############################################################################
- E-ACSL [2020/03/10] Call E-ACSL's free functions for globals in a
@@ -27,7 +27,7 @@
`__e_acsl_delete_block` in presence of gotos to return statements.
- E-ACSL [2020/03/09] Improve verdict messages emitted by e_acsl_assert.
-* E-ACSL [2020/01/06] Fix typing bug in presence of variable-length
- arrays that may lead to incorrect generated code.
+ arrays that may lead to incorrect generated code.
-* E-ACSL [2019/12/04] Fix bug with compiler built-ins.
############################
@@ -36,26 +36,26 @@ Plugin E-ACSL 20.0 (Calcium)
- E-ACSL [2019/08/28] Support of rational numbers and operations.
-! E-ACSL [2019/08/28] Deactivate the unsound support of real
- numbers (that are not rationals). They were previously
- unsoundly converted to floating point numbers.
+ numbers (that are not rationals). They were previously
+ unsoundly converted to floating point numbers.
##############################
Plugin E-ACSL 19.0 (Potassium)
##############################
- E-ACSL [2019/04/29] Support for logic functions and predicates
- without labels.
+ without labels.
- runtime [2019/02/26] The behavior of __e_acsl_assert now depends on the
- runtime value of the global variable __e_acsl_sound_verdict:
- if 0, it means that its verdict is possibly incorrect.
+ runtime value of the global variable __e_acsl_sound_verdict:
+ if 0, it means that its verdict is possibly incorrect.
- E-ACSL [2019/02/26] New option -e-acsl-instrument to instrument
- only a specified set of functions. It may lead to incorrect
- verdicts.
+ only a specified set of functions. It may lead to incorrect
+ verdicts.
- E-ACSL [2019/02/19] New option -e-acsl-functions to monitor only
- annotations in a white list of functions.
+ annotations in a white list of functions.
-* runtime [2019/02/04] Fix initialization of the E-ACSL runtime in
- presence of multiple calls to its initializer (for
- instance, if the main is a recursive function).
+ presence of multiple calls to its initializer (for
+ instance, if the main is a recursive function).
-* runtime [2019/01/02] Fix overlap of TLS with other memory
segments for large memory spaces.
- E-ACSL [2018/11/15] Predicates with empty quantifications
@@ -87,21 +87,21 @@ Plugin E-ACSL Chlorine-20180501
- E-ACSL [2018/03/30] Support for let binding.
- E-ACSL [2018/02/21] New option -e-acsl-replace-libc-functions to
- replace a few libc functions by built-ins that efficiently
- detects when they are incorrectly called.
+ replace a few libc functions by built-ins that efficiently
+ detects when they are incorrectly called.
- E-ACSL [2018/02/21] New option -e-acsl-validate-format-strings to
- detect format string errors in printf-like functions.
+ detect format string errors in printf-like functions.
-* E-ACSL [2018/02/21] Correct support of variable-length array
- (fix bug #1834).
+ (fix bug #1834).
-* runtime [2018/02/16] Function __e_acsl_offset now returns size_t.
-* E-ACSL [2018/02/07] Fix incorrect typing in presence of
- comparison operators (may only be visible when directly
- analyzing the E-ACSL's generated code with Frama-C without
- pretty-printing it).
+ comparison operators (may only be visible when directly
+ analyzing the E-ACSL's generated code with Frama-C without
+ pretty-printing it).
-* runtime [2018/01/30] E-ACSL aborted when run on a machine with a
- low hard limit on the stack size.
+ low hard limit on the stack size.
-* E-ACSL [2018/01/08] Fix a crash when translating a postcondition
- that should generate a local variable (bts #2339).
+ that should generate a local variable (bts #2339).
-* e-acsl-gcc [2017/11/28] Several files may be given to e-acsl-gcc.sh
(as specified).
-* E-ACSL [2017/11/27] Fix 'segmentation fault' of the generated monitor
@@ -134,28 +134,28 @@ Plugin E-ACSL Phosphorus-20170515
#################################
- runtime [2017/03/29] The (much more efficient) shadow memory model is
- now used by default.
+ now used by default.
-* runtime [2017/03/28] Fix backtrace when the failed instrumented programs
- do not require memory model.
+ do not require memory model.
-! 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
- to check the integrity of the generated AST before
- instrumentation.
+ to check the integrity of the generated AST before
+ instrumentation.
-! 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
- memory properties when early exiting a block through
- goto, break or continue.
+ memory properties when early exiting a block through
+ goto, break or continue.
-* E-ACSL [2017/03/01] Correct support of stdin, stdout and stderr
- in annotations.
+ in annotations.
-* E-ACSL [2017/02/24] Fix crash with casts from non-integral terms to
- integral types (bts #2284).
+ integral types (bts #2284).
-* E-ACSL [2017/02/17] Fix bug with goto which points to a labeled
- statement which must be instrumented.
+ statement which must be instrumented.
-* E-ACSL [2017/01/23] Fix bug #2252 about pointer arithmetic with
- negative offsets.
+ negative offsets.
-* E-ACSL [2017/01/23] Fix bug with typing of unary and binary
- operations in a few cases: the generated code might have
- overflowed.
+ operations in a few cases: the generated code might have
+ overflowed.
#########################
Plugin E-ACSL 0.8 Silicon
@@ -163,71 +163,71 @@ Plugin E-ACSL 0.8 Silicon
-* 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.
- --enable-optimized-rtl configure option removed
+ --enable-optimized-rtl configure option removed
-* configure [2016/08/02] Added --enable-optimized-rtl option to configure
-* e-acsl-gcc [2016/08/02] Removed --production|-P, --no-stdlib|-N and
- --debug-log|-D options of e-acsl-gcc.sh.
+ --debug-log|-D options of e-acsl-gcc.sh.
-* E-ACSL [2016/07/21] Enable reporting of stack traces during assertion
- failures in instrumented programs.
+ failures in instrumented programs.
-* e-acsl-gcc [2016/07/13] Add an e-acsl-gcc.sh option (--print--models)
- allowing to print the names of the supported memory models.
+ allowing to print the names of the supported memory models.
-* E-ACSL [2016/07/01] Add monitoring support for aligned memory
- allocation via posix_memalign and aligned alloc functions.
+ allocation via posix_memalign and aligned alloc functions.
-* runtime [2016/07/01] Add local version of GMP library customized for use
- with E-ACSL runtime library.
+ with E-ACSL runtime library.
-* runtime [2016/07/01] Add custom implementation of malloc for use with
- E-ACSL runtime library (via jemalloc library).
+ E-ACSL runtime library (via jemalloc library).
- E-ACSL [2016/05/31] New option -e-acsl-builtins which allows to
- declare pure C functions which can be used in logic
- function application.
+ declare pure C functions which can be used in logic
+ function application.
- E-ACSL [2016/05/23] Re-implementation of the type system which
- improves the efficiency of the generated code over integers.
+ improves the efficiency of the generated code over integers.
-* E-ACSL [2016/05/23] Fix bug #2191 about complicate structs and
- literate string.
+ literate string.
-* e-acsl-gcc [2016/05/22] Add an e-acsl-gcc.sh option (--rte|-a) allowing to
- annotate the source program with memory-safety assertions prior
- to instrumentation.
+ annotate the source program with memory-safety assertions prior
+ to instrumentation.
-* 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
- initialization of tracked memory blocks in the E-ACSL
- memory model library.
+ initialization of tracked memory blocks in the E-ACSL
+ memory model library.
###########################
Plugin E-ACSL 0.6 Magnesium
###########################
-* e-acsl-gcc [2016/01/22] Add an e-acsl-gcc.sh option allowing to skip
- compilation of original sources.
+ compilation of original sources.
-* Makefile [2016/01/15] Fix installation with custom --prefix.
-* runtime [2016/01/05] Fix bug in the memory model that caused the
- tracked size of heap memory be computed incorrectly.
+ tracked size of heap memory be computed incorrectly.
- e-acsl-gcc [2015/12/15] Add a convenience script e-acsl-gcc.sh for
- small runs of the E-ACSL plugin.
+ small runs of the E-ACSL plugin.
-* E-ACSL [2015/12/08] Fix bug #1817 about incorrect initialization of
- literal strings in global arrays with compound initializers.
+ literal strings in global arrays with compound initializers.
-* runtime [2015/11/06] Fix a crash occuring when using a recent libc
- while GMP headers provided by E-ACSL are used.
+ while GMP headers provided by E-ACSL are used.
########################
Plugin E-ACSL 0.5 Sodium
########################
- E-ACSL [2015/06/01] Support of \freeable. Thus illegal calls to
- free (e.g. double free) are detected.
+ free (e.g. double free) are detected.
-* 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
- default (easier to use declarations like __memory_size).
+ default (easier to use declarations like __memory_size).
- E-ACSL [2015/05/27] Compatibility with new Frama-C Sodium option
- -frama-c-stdlib.
+ -frama-c-stdlib.
-* E-ACSL [2015/04/28] Fix bug when using fopen.
-* E-ACSL [2015/03/06] Fix bugs #1636 and #1837 about scoping of literal
- strings.
+ strings.
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
- type used in a floating point/real context in an annotation.
+ type used in a floating point/real context in an annotation.
########################
Plugin E-ACSL 0.4.1 Neon
@@ -238,22 +238,22 @@ Plugin E-ACSL 0.4.1 Neon
-* 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
- computing the block which a pointer points to.
+ computing the block which a pointer points to.
-* E-ACSL [2014/07/08] Fix bug #1695 about using some part of the
- (Frama-C) libc which prevents linking of the generated C code.
+ (Frama-C) libc which prevents linking of the generated C code.
-* E-ACSL [2014/05/21] Fix bug #1782 about incorrect URL in the
- documentation.
+ documentation.
- E-ACSL [2014/03/27] Remove spurious warnings when using type real
- numbers.
+ numbers.
-* E-ACSL [2014/03/26] Fix bug #1692 about wrong localisation of
- some messages.
+ some messages.
- E-ACSL [2014/03/26] Remove a spurious warning when an annotated
- function is first declared, then defined.
+ function is first declared, then defined.
-* E-ACSL [2014/03/26] Fix bug #1717 about instrumentation of
- labeled statements.
+ labeled statements.
-* 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
- generates incorrect code.
+ generates incorrect code.
-* E-ACSL [2014/03/17] Fix bug #1700 about non-ISO empty struct.
###############################
@@ -261,9 +261,9 @@ Plugin E-ACSL 0.4 Neon_20140301
###############################
-* E-ACSL [2014/01/28] Fix bug #1634 occuring in presence of static
- addresses.
+ addresses.
-* E-ACSL [2013/09/26] Fix incorrectness which may occur in presence
- of aliasing.
+ of aliasing.
-* E-ACSL [2013/09/25] Some loop invariants were tagged as "assertions".
###################################
@@ -271,19 +271,19 @@ Plugin E-ACSL 0.3 Fluorine_20130601
###################################
- E-ACSL [2013/09/18] More precise message for unsupported contract
- clauses.
+ clauses.
- 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
- initializers (bts #1478).
+ initializers (bts #1478).
-* E-ACSL [2013/09/04] Fix bug when mixing -e-acsl-prepare and
- running E-ACSL in another project (bts #!1473).
+ running E-ACSL in another project (bts #!1473).
-* 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
- generated project.
+ generated project.
-* E-ACSL [2013/05/30] Fix -e-acsl-debug n, with n >= 2.
###################################
@@ -291,18 +291,18 @@ Plugin E-ACSL 0.2 Fluorine_20130401
###################################
- E-ACSL [2013/01/09] New option -e-acsl-valid. By default, valid
- annotation are not translated anymore.
+ annotation are not translated anymore.
-* E-ACSL [2013/01/09] Fix bug when translating a postcondition of a
- function where the init state is the same than the final
- state (bts #!1300).
+ function where the init state is the same than the final
+ state (bts #!1300).
- 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
- uninitialized variables.
+ uninitialized variables.
- E-ACSL [2012/11/19] Support of floats in annotations. Approximate
- reals by floats.
+ reals by floats.
- 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.
@@ -310,25 +310,25 @@ Plugin E-ACSL 0.2 Fluorine_20130401
- 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
- even if one fails.
+ even if one fails.
- runtime [2012/04/27] Improve ACSL spec of E-ACSL' C library.
-* Makefile [2012/01/27] Fix compilation bug when configuring with
- --enable-external.
-- E-ACSL [2012/01/25] Nicer generated variable names.
+ --enable-external.
+- 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
- standard assert.
-- E-ACSL [2012/01/23] Support of bitwise complementation.
-- E-ACSL [2012/01/20] Use GMP arithmetics only when required
- (i.e. mostly never in practice).
+ standard assert.
+- E-ACSL [2012/01/23] Support of bitwise complementation.
+- E-ACSL [2012/01/20] Use GMP arithmetics only when required
+ (i.e. mostly never in practice).
###################################
Plugin E-ACSL 0.1 Nitrogen_20111001
###################################
-- E-ACSL [2012/01/06] First public release.
+- E-ACSL [2012/01/06] First public release.
###################################