Newer
Older
###############################################################################
# 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 #
# For compatibility with old change log formats: #
# '#?nnn' : OLD-BTS entry #nnn #
###############################################################################
# Categories:
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
#################################
Plugin E-ACSL Phosphorus-20170515
#################################
-! E-ACSL [2017/05/19] Add --temporal option to e-acsl.gcc.sh
-! E-ACSL [2017/05/19] Enable analysis for temporal errors in E-ACSL
-! E-ACSL [2017/03/26] Add --weak-validity option to e-acsl.gcc.sh
-! E-ACSL [2017/03/26] Add --rt-verbose option to e-acsl.gcc.sh
-! E-ACSL [2017/03/26] Add --keep-going option to e-acsl.gcc.sh allowing
a program to continue execution after an assertion failure
-! E-ACSL [2017/03/26] Add --stack-size and --heap-size options to
e-acsl-gcc.sh allowing to change the default sizes of the
respective shadow spaces
- E-ACSL [2017/03/29] The (much more efficient) shadow memory model is
now used by default.
-* E-ACSL [2017/03/28] Fix backtrace when the failed instrumented programs
do not require memory model.
-! E-ACSL [2017/03/19] Remove --print|-p option from e-acsl-gcc.sh
-! E-ACSL [2017/03/16] Add --check option to e-acsl-gcc.sh which allows
to check the integrity of the generated AST before
instrumentation.
-! E-ACSL [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.
-* E-ACSL [2017/03/01] Correct support of stdin, stdout and stderr
in annotations.
-* E-ACSL [2017/02/24] Fix crash with casts from non-integral terms to
integral types (bts #2284).
Julien Signoles
committed
-* E-ACSL [2017/02/17] Fix bug with goto which points to a labeled
statement which must be instrumented.
-* E-ACSL [2017/01/23] Fix bug #2252 about pointer arithmetic with
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.
#########################
Plugin E-ACSL 0.8 Silicon
#########################
Kostyantyn Vorobyov
committed
-* E-ACSL [2016/11/07] Added --rte-select feature to e-acsl-gcc.sh.
Kostyantyn Vorobyov
committed
-* E-ACSL [2016/08/02] Added --rt-debug feature to e-acsl-gcc.sh.
--enable-optimized-rtl configure option removed
Kostyantyn Vorobyov
committed
-* E-ACSL [2016/08/02] Added --enable-optimized-rtl option to configure
-* E-ACSL [2016/08/02] Removed --production|-P, --no-stdlib|-N and
--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.
-* E-ACSL [2016/07/13] Add an e-acsl-gcc.sh option (--print--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.
-* E-ACSL [2016/07/01] Add local version of GMP library customized for use
with E-ACSL runtime library.
-* E-ACSL [2016/07/01] Add custom implementation of malloc for use with
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.
Julien Signoles
committed
- E-ACSL [2016/05/23] Re-implementation of the type system which
improves the efficiency of the generated code over integers.
-* E-ACSL [2016/05/23] Fix bug #2191 about complicate structs and
literate string.
-* E-ACSL [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.
Julien Signoles
committed
-* E-ACSL [2016/05/23] Fix bug #1395 about recursive functions.
Julien Signoles
committed
-* E-ACSL [2016/04/07] Fix 'make install' when executed within Frama-C.
-* E-ACSL [2016/03/31] Improve performance of Patricia Trie memory model.
-* E-ACSL [2016/02/25] Fix 'make clean' in tests.
-* E-ACSL [2016/01/15] Fix several bugs related to incorrect partial
initialization of tracked memory blocks in the E-ACSL runtime
library.
###########################
Plugin E-ACSL 0.6 Magnesium
###########################
-* E-ACSL [2016/01/22] Add an e-acsl-gcc.sh option allowing to skip
Kostyantyn Vorobyov
committed
compilation of original sources.
Kostyantyn Vorobyov
committed
-* E-ACSL [2016/01/15] Fix installation with custom --prefix.
-* E-ACSL [2016/01/05] Fix bug in the memory model that caused the
tracked size of heap memory be computed incorrectly.
- E-ACSL [2015/12/15] Add a convenience script e-acsl-gcc.sh for
Kostyantyn Vorobyov
committed
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.
-* E-ACSL [2015/11/06] Fix a crash occuring when using a recent libc
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.
-* 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).
- E-ACSL [2015/05/27] Compatibility with new Frama-C Sodium option
-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.
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.
########################
Plugin E-ACSL 0.4.1 Neon
########################
-* 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/07/19] Fix bug #1836 about one-off error when
computing the block which a pointer points to.
-* E-ACSL [2014/07/08] Fix bug #1695 about using some part of the
Julien Signoles
committed
(Frama-C) libc which prevents linking of the generated C code.
Julien Signoles
committed
-* E-ACSL [2014/05/21] Fix bug #1782 about incorrect URL in the
documentation.
- E-ACSL [2014/03/27] Remove spurious warnings when using type real
numbers.
-* E-ACSL [2014/03/26] Fix bug #1692 about wrong localisation of
some messages.
Julien Signoles
committed
- E-ACSL [2014/03/26] Remove a spurious warning when an annotated
function is first declared, then defined.
-* E-ACSL [2014/03/26] Fix bug #1717 about instrumentation of
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
Julien Signoles
committed
generates incorrect code.
-* E-ACSL [2014/03/17] Fix bug #1700 about non-ISO empty struct.
###############################
Plugin E-ACSL 0.4 Neon_20140301
###############################
-* E-ACSL [2014/01/28] Fix bug #1634 occuring in presence of static
addresses.
-* E-ACSL [2013/09/26] Fix incorrectness which may occur in presence
of aliasing.
-* E-ACSL [2013/09/25] Some loop invariants were tagged as "assertions".
###################################
Plugin E-ACSL 0.3 Fluorine_20130601
###################################
- E-ACSL [2013/09/18] More precise message for unsupported contract
clauses.
-* E-ACSL [2013/09/18] Fix bug which may occur with divisions and modulos.
- E-ACSL [2013/09/10] Improve ACSL contracts of the E-ACSL C library.
- E-ACSL [2013/09/06] Support of loop invariants.
Julien Signoles
committed
-* E-ACSL [2013/09/04] Fix bug when monitored global variables have
initializers (bts #1478).
Julien Signoles
committed
-* E-ACSL [2013/09/04] Fix bug when mixing -e-acsl-prepare and
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.
-* E-ACSL [2013/05/30] Fix -e-acsl-debug n, with n >= 2.
###################################
Plugin E-ACSL 0.2 Fluorine_20130401
###################################
Julien Signoles
committed
- E-ACSL [2013/01/09] New option -e-acsl-valid. By default, valid
annotation are not translated anymore.
Julien Signoles
committed
-* 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).
- 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.
Julien Signoles
committed
- E-ACSL [2012/11/27] Prevent runtime errors in annotations, except
Julien Signoles
committed
- E-ACSL [2012/11/19] Support of floats in annotations. Approximate
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.
- 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
even if one fails.
- E-ACSL [2012/04/27] Improve ACSL spec of E-ACSL' C library.
-* E-ACSL [2012/01/27] Fix compilation bug when configuring with
--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.
- E-ACSL [2012/01/24] Function e_acsl_assert now consistent with
- E-ACSL [2012/01/23] Support of bitwise complementation.
- E-ACSL [2012/01/20] Use GMP arithmetics only when required
###################################
Plugin E-ACSL 0.1 Nitrogen_20111001
###################################
- E-ACSL [2012/01/06] First public release.
###################################