Forked from
pub / frama-c
18167 commits behind the upstream repository.
-
Fonenantsoa Maurica authored
- Safe locations are ok but need to increase TLS to 32 Mo for the libxml usecase - Fix order of operations during memory initialization - TODO: memory allocated before main are not seen as being valid
Fonenantsoa Maurica authored- Safe locations are ok but need to increase TLS to 32 Mo for the libxml usecase - Fix order of operations during memory initialization - TODO: memory allocated before main are not seen as being valid
To find the state of this project's repository at the time of any of these versions, check out the tags.
Changelog 14.58 KiB
###############################################################################
# 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 monitor generation
# runtime C runtime library (and memory model)
# e-acsl-gcc launcher e-acsl-gcc.sh
# Makefile Makefile
# configure configure
###############################################################################
##########################
Plugin E-ACSL 18.0 (Argon)
##########################
-* runtime [2018/11/13] Fix bug #!2405 about memory initialization
in presence of GCC constructors.
-* E-ACSL [2018/10/23] Fix bug #2406 about monitoring of variables
with incomplete types.
-* E-ACSL [2018/10/04] Fix bug #2386 about incorrect typing when
performing pointer subtraction.
-* E-ACSL [2018/10/04] Support for \at on purely logic variables.
Fix bug #1762 about out-of-scope variables when using \old.
-* E-ACSL [2018/10/02] Fix bug #2305 about taking the address of a
bitfield.
- E-ACSL [2018/09/18] Support for ranges in memory builtins
(\valid, \initialized, etc).
###############################
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.
- E-ACSL [2018/02/21] New option -e-acsl-validate-format-strings to
detect format string errors in printf-like functions.
-* E-ACSL [2018/02/21] Correct support of variable-length array
(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).
-* runtime [2018/01/30] E-ACSL aborted when run on a machine with a
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).
-* 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
whenever the main has a precondition depending on the memory
model.
-* E-ACSL [2017/11/27] Restore behavior of option -e-acsl-valid broken
since Phosphorus (included).
#############################
Plugin E-ACSL Sulfur-20171101
#############################
-* E-ACSL [2017/10/25] Fix bug #2303 about unnamed formals in
annotated functions.
- 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
through -e-acsl-temporal-validity (disabled by default).
- 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
a program to continue execution after an assertion failure.
- e-acsl-gcc [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.
#################################
Plugin E-ACSL Phosphorus-20170515
#################################
- runtime [2017/03/29] The (much more efficient) shadow memory model is
now used by default.
-* runtime [2017/03/28] Fix backtrace when the failed instrumented programs
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.
-! 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.
-* 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).
-* 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
#########################
-* 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
-* 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.
-* E-ACSL [2016/07/21] Enable reporting of stack traces during assertion
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.
-* E-ACSL [2016/07/01] Add monitoring support for aligned memory
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.
-* runtime [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.
- 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-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.
-* 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.
###########################
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.
-* 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.
- e-acsl-gcc [2015/12/15] Add a convenience script e-acsl-gcc.sh for
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.
-* runtime [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/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.
-* 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.
-* 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.
- 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 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] 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).
-* 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
###################################
- E-ACSL [2013/01/09] New option -e-acsl-valid. By default, valid
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).
- 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.
- 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.
- 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.
-* 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).
###################################
Plugin E-ACSL 0.1 Nitrogen_20111001
###################################
- E-ACSL [2012/01/06] First public release.
###################################