Skip to content
Snippets Groups Projects
Commit 81bddcd0 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl:doc] Replace tabs with spaces in changelog

parent 92405206
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/doc/Changelog
+ 89
− 89
View file @ 81bddcd0
......@@ -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.
###################################
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment