diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 1eeeb2ac090f234f3b50fa4f15899cbe7089b7c9..2c736f3ce0e475fa120daa21c169bd24616acc8c 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,29 +19,29 @@
# configure configure
###############################################################################
--* E-ACSL [2020/03/24] Fix automatic deactivation of plug-in Variadic when
+-* E-ACSL [2020-03-24] Fix automatic deactivation of plug-in Variadic when
E-ACSL is directly called from Frama-C without using
e-acsl-gcc.sh.
-- E-ACSL [2020/03/10] Call E-ACSL's free functions for globals in a
+- E-ACSL [2020-03-10] Call E-ACSL's free functions for globals in a
separate function at the end of main.
-- E-ACSL [2020/03/10] Call `__e_acsl_memory_init` only if the memory
+- E-ACSL [2020-03-10] Call `__e_acsl_memory_init` only if the memory
model analysis is running.
--* E-ACSL [2020/03/10] Fix frama-c/e-acsl#105 about misplaced
+-* E-ACSL [2020-03-10] Fix frama-c/e-acsl#105 about misplaced
`__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/03/16] Fix #?1386 and frama-c/e-acsl#91 about the tracking
+- E-ACSL [2020-03-09] Improve verdict messages emitted by e_acsl_assert.
+-* E-ACSL [2020-03-16] Fix #?1386 and frama-c/e-acsl#91 about the tracking
of variables declared inside the body of switches.
-- 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
+- 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
arrays that may lead to incorrect generated code.
--* E-ACSL [2019/12/04] Fix bug with compiler built-ins.
+-* E-ACSL [2019-12-04] Fix bug with compiler built-ins.
############################
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
+- 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.
@@ -49,292 +49,292 @@ Plugin E-ACSL 20.0 (Calcium)
Plugin E-ACSL 19.0 (Potassium)
##############################
-- E-ACSL [2019/04/29] Support for logic functions and predicates
+- E-ACSL [2019-04-29] Support for logic functions and predicates
without labels.
-- runtime [2019/02/26] The behavior of __e_acsl_assert now depends on the
+- 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.
-- E-ACSL [2019/02/26] New option -e-acsl-instrument to instrument
+- E-ACSL [2019-02-26] New option -e-acsl-instrument to instrument
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
+- E-ACSL [2019-02-19] New option -e-acsl-functions to monitor only
annotations in a white list of functions.
--* runtime [2019/02/04] Fix initialization of the E-ACSL runtime in
+-* 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).
--* runtime [2019/01/02] Fix overlap of TLS with other memory
+-* 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
+- E-ACSL [2018-11-15] Predicates with empty quantifications
directly generate \true or \false instead of nested loops.
##########################
Plugin E-ACSL 18.0 (Argon)
##########################
--* E-ACSL [2018/11/13] Fix typing bug in quantifications when the
+-* E-ACSL [2018-11-13] Fix typing bug in quantifications when the
guards of the quantifier variable cannot be represented into
its type.
--* runtime [2018/11/13] Fix bug #!2405 about memory initialization
+-* 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
+-* 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
+-* 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.
+-* 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
+-* 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
+- E-ACSL [2018-09-18] Support for ranges in memory builtins
(\valid, \initialized, etc).
-###############################
-Plugin E-ACSL Chlorine-20180501
-###############################
+######################################
+Plugin E-ACSL 17.0 (Chlorine-20180501)
+######################################
-- E-ACSL [2018/03/30] Support for let binding.
-- E-ACSL [2018/02/21] New option -e-acsl-replace-libc-functions to
+- 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
+- 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
+-* 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
+-* 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
+-* 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
+-* 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
+-* 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
+-* 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
+-* E-ACSL [2017-11-27] Restore behavior of option -e-acsl-valid broken
since Phosphorus (included).
-#############################
-Plugin E-ACSL Sulfur-20171101
-#############################
+####################################
+Plugin E-ACSL 16.0 (Sulfur-20171101)
+####################################
--* E-ACSL [2017/10/25] Fix bug #2303 about unnamed formals in
+-* 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
+- 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
+- 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 [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
-#################################
+########################################
+Plugin E-ACSL 15.0 (Phosphorus-20170515)
+########################################
-- runtime [2017/03/29] The (much more efficient) shadow memory model is
+- 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
+-* 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
+-! 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
+-! 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
+-* 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
+-* 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
+-* 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
+-* 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
+-* 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
-#########################
+###########################
+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.
+-* 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
+-* 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
+-* 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)
+-* 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
+-* 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
+-* 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
+-* 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
+- 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
+- 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
+-* 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
+-* 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
+-* 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
-###########################
+#############################
+Plugin E-ACSL 0.6 (Magnesium)
+#############################
--* e-acsl-gcc [2016/01/22] Add an e-acsl-gcc.sh option allowing to skip
+-* 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
+-* 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
+- 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
+-* 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
+-* 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
-########################
+##########################
+Plugin E-ACSL 0.5 (Sodium)
+##########################
-- E-ACSL [2015/06/01] Support of \freeable. Thus illegal calls to
+- 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
+-* 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
+- 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
+-* 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
+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
-########################
+##########################
+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
+-* 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
+-* 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
+-* 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
+- 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
+-* 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
+- 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
+-* 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
+-* 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.
+-* E-ACSL [2014-03-17] Fix bug #1700 about non-ISO empty struct.
-###############################
-Plugin E-ACSL 0.4 Neon_20140301
-###############################
+#################################
+Plugin E-ACSL 0.4 (Neon_20140301)
+#################################
--* E-ACSL [2014/01/28] Fix bug #1634 occuring in presence of static
+-* 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
+-* 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".
+-* E-ACSL [2013-09-25] Some loop invariants were tagged as "assertions".
-###################################
-Plugin E-ACSL 0.3 Fluorine_20130601
-###################################
+#####################################
+Plugin E-ACSL 0.3 (Fluorine_20130601)
+#####################################
-- E-ACSL [2013/09/18] More precise message for unsupported contract
+- 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
+- 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
+-* 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
+-* 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.
+-* E-ACSL [2013-05-30] Fix -e-acsl-debug n, with n >= 2.
-###################################
-Plugin E-ACSL 0.2 Fluorine_20130401
-###################################
+#####################################
+Plugin E-ACSL 0.2 (Fluorine_20130401)
+#####################################
-- E-ACSL [2013/01/09] New option -e-acsl-valid. By default, valid
+- 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
+-* 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
+- 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
+- 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
+- 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
+- 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
+- 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
+- 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
-###################################
+#####################################
+Plugin E-ACSL 0.1 (Nitrogen_20111001)
+#####################################
-- E-ACSL [2012/01/06] First public release.
+- E-ACSL [2012-01-06] First public release.
###################################
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 8e42d3b2e3f604b8871d8b11ebcd4961744b2af8..4ba62abcdd056cc8f9e218c5ee07a4195e541d78 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,463 +20,443 @@
# <Prover>: prover
###############################################################################
- - WP [2020/04/10] Full support for Why3 IEEE float library
- - WP [2020/04/10] Removed option -wp-check
- - WP [2020/04/09] Added smoke tests for dead call (-wp-smoke-dead-call)
- - WP [2020/03/23] Added smoke tests for dead code (-wp-smoke-dead-code)
- - WP [2020/03/23] Added smoke tests for dead loop (-wp-smoke-dead-loop)
- - WP [2020/03/26] Added support for invalid-pointer predicate
- - WP [2020/03/04] Fixed scope problem on block outgoing edge
- - WP [2020/02/21] Why3 prover version fallback
- - WP [2020/02/21] Why3 prover full-names use ':' instead of ','
- - WP [2020/02/20] Fixes handling of LoopCurrent in loop invariants
- - WP [2020/02/10] Specify cache mode with FRAMAC_WP_CACHE=<mode> (-wp-cache-env)
- - WP [2020/02/10] Update scripts with FRAMAC_WP_SCRIPT=update and -wp-prover script
- - WP [2020/02/10] Move frame conditions to Type section for better filtering
- - WP [2020/02/10] Extended frame conditions to pointers inside compound
- - WP [2020/02/10] Extended frame conditions with global C-types
- - WP [2019/17/04] Control splitting with -wp-max-split <n>
- - WP [2019/12/19] Fix drivers in different projects
- - WP [2019/12/04] Added option -wp-run-all-provers
- - WP [2019/06/04] Checks for inconsistent requires (-wp-smoke-tests)
- - WP [2019/01/29] Emit a warning when no goal is generated
- - WP [2018/04/17] Limit the number of splits (see -wp-max-split)
- - TIP [2018/04/03] Create session directory only on demand
- - TIP [2018/03/19] Specification of JSON script format
- - WP [2018/03/18] Additional lemma about remainder (mod)
- - TIP [2018/03/18] Refactor structure of session directory (remove models)
- - TIP [2018/02/20] Extends bitwise tactics to dis-equalities
- - WP [2018/02/18] Additional lemmas about logical shift compositions
+ - WP [2020-04-10] Full support for Why3 IEEE float library
+ - WP [2020-04-10] Removed option -wp-check
+ - WP [2020-04-09] Added smoke tests for dead call (-wp-smoke-dead-call)
+ - WP [2020-03-23] Added smoke tests for dead code (-wp-smoke-dead-code)
+ - WP [2020-03-23] Added smoke tests for dead loop (-wp-smoke-dead-loop)
+ - WP [2020-03-26] Added support for invalid-pointer predicate
+ - WP [2020-03-04] Fixed scope problem on block outgoing edge
+ - WP [2020-02-21] Why3 prover version fallback
+ - WP [2020-02-21] Why3 prover full-names use ':' instead of ','
+ - WP [2020-02-20] Fixes handling of LoopCurrent in loop invariants
+ - WP [2020-02-10] Specify cache mode with FRAMAC_WP_CACHE=<mode> (-wp-cache-env)
+ - WP [2020-02-10] Update scripts with FRAMAC_WP_SCRIPT=update and -wp-prover script
+ - WP [2020-02-10] Move frame conditions to Type section for better filtering
+ - WP [2020-02-10] Extended frame conditions to pointers inside compound
+ - WP [2020-02-10] Extended frame conditions with global C-types
+ - WP [2019-17-04] Control splitting with -wp-max-split <n>
+ - WP [2019-12-19] Fix drivers in different projects
+ - WP [2019-12-04] Added option -wp-run-all-provers
+ - WP [2019-06-04] Checks for inconsistent requires (-wp-smoke-tests)
+ - WP [2019-01-29] Emit a warning when no goal is generated
+ - WP [2018-04-17] Limit the number of splits (see -wp-max-split)
+ - TIP [2018-04-03] Create session directory only on demand
+ - TIP [2018-03-19] Specification of JSON script format
+ - WP [2018-03-18] Additional lemma about remainder (mod)
+ - TIP [2018-03-18] Refactor structure of session directory (remove models)
+ - TIP [2018-02-20] Extends bitwise tactics to dis-equalities
+ - WP [2018-02-18] Additional lemmas about logical shift compositions
##########################
Plugin WP 20.0 (Calcium)
##########################
-- TIP [2019/09/17] Using all selected Why-3 provers for proof search
-- Gui [2019/09/17] Updated panel for provers, models, cache, etc.
-- WP [2019/09/12] New cache mechanism for why3 provers, see -wp-cache option
--! WP [2019/09/17] Deprecated native alt-ergo & coq output, see -wp-prover option
-- WP [2019/09/16] Deprecated & Renamed -wp-script into -wp-coq-script
-- WP [2019/09/16] Deprecated & Renamed -wp-update-script into -wp-update-coq-script
-- WP [2019/09/16] Deprecated & Renamed -wp-tactic into -wp-coq-tactic
-- WP [2019/09/16] Deprecated & Renamed -wp-tryhints into -wp-coq-tryhints
-- WP [2019/09/16] Deprecated & Renamed -wp-hints into -wp-coq-hints
-- WP [2019/09/16] Renamed -wp-why-opt into -wp-why3-opt
-- WP [2019/09/16] Renamed -wp-init-alias into -wp-alias-init
-- WP [2019/09/16] Removed -wp-include
-- WP [2019/09/16] Removed -wp-why3
-- WP [2019/09/16] Removed -wp-why-lib
-- WP [2019/09/16] Removed -wp-depth
-- WP [2019/09/16] Default -wp-extensional changed to true
-- WP [2019/09/16] Default -wp-init-const changed to true
--! WP [2019/07/05] Default -wp-prover <p> changed to <why3:p> (including default alt-ergo)
--! WP [2019/07/05] Use native Why3 API (now requires why3 at compile time)
-- WP [2019/06/27] Improving Cint simplifier and quantifier introduction
-o Qed [2019/06/27] More secure API for quantifier management
-- Qed [2019/05/09] Transform (some) boolean quantifications into variable assignments
+- TIP [2019-09-17] Using all selected Why-3 provers for proof search
+- Gui [2019-09-17] Updated panel for provers, models, cache, etc.
+- WP [2019-09-12] New cache mechanism for why3 provers, see -wp-cache option
+-! WP [2019-09-17] Deprecated native alt-ergo & coq output, see -wp-prover option
+- WP [2019-09-16] Deprecated & Renamed -wp-script into -wp-coq-script
+- WP [2019-09-16] Deprecated & Renamed -wp-update-script into -wp-update-coq-script
+- WP [2019-09-16] Deprecated & Renamed -wp-tactic into -wp-coq-tactic
+- WP [2019-09-16] Deprecated & Renamed -wp-tryhints into -wp-coq-tryhints
+- WP [2019-09-16] Deprecated & Renamed -wp-hints into -wp-coq-hints
+- WP [2019-09-16] Renamed -wp-why-opt into -wp-why3-opt
+- WP [2019-09-16] Renamed -wp-init-alias into -wp-alias-init
+- WP [2019-09-16] Removed -wp-include
+- WP [2019-09-16] Removed -wp-why3
+- WP [2019-09-16] Removed -wp-why-lib
+- WP [2019-09-16] Removed -wp-depth
+- WP [2019-09-16] Default -wp-extensional changed to true
+- WP [2019-09-16] Default -wp-init-const changed to true
+-! WP [2019-07-05] Default -wp-prover <p> changed to <why3:p> (including default alt-ergo)
+-! WP [2019-07-05] Use native Why3 API (now requires why3 at compile time)
+- WP [2019-06-27] Improving Cint simplifier and quantifier introduction
+o Qed [2019-06-27] More secure API for quantifier management
+- Qed [2019-05-09] Transform (some) boolean quantifications into variable assignments
##########################
Plugin WP 19.0 (Potassium)
##########################
-- Wp [2019/05/09] Fixes -wp-simplify-is-cint simplifier
-- Wp [2019/04/26] Now requires -warn-invalid-bool
-- Wp [2019/04/26] Removed option -wp-bool-range
-- Wp [2019/04/24] Support for Why3 1.* and Coq 8.{7-9}
-- Wp [2019/02/26] Support for @check ACSL annotations
-- WP [2018/02/16] Filter out some variables from separation
-- TIP [2018/02/15] Extend bitwise-eq auto-strategy on hypotheses
-- TIP [2018/02/15] Fix wrong reconciliation of sub-scripts during replay
-- Wp [2018/02/15] Better naming convention, consistent with report-classify
-- WP [2019/02/05] Auto filter properties with name "no_wp:"
-- Wp [2019/01/28] Now -wp-dynamic is set by default (annotation @calls)
-- Wp [2019/01/28] New floating-point model
-- Wp [2018/01/18] Auto-Search mode, see -wp-auto
-- TIP [2018/01/18] Auto-Search mode from the GUI
-- TIP [2018/01/18] New Strategies for bitwise and congruence operations
-- TIP [2017/12/17] Fix bug that makes the TIP wrongly reuse previous results
-- Wp [2017/12/17] Option -wp-print-separation changed into -wp-warn-separation
-- Wp [2017/12/17] Option -wp-unfold-assigns for proving assigns of aggregates field by field
-- TIP [2017/04/25] New tactical Congruence (divisions and products)
-- Qed [2017/10/30] Extends simplifications for lsl,lsr and div
-- Wp [2017/10/27] Fix soundness bug when assigning non-valid ranges
-- Qed [2017/10/27] New simplifications for validity and ranges
-- TIP [2017/10/27] New tacticals for validity and ranges
+- Wp [2019-05-09] Fixes -wp-simplify-is-cint simplifier
+- Wp [2019-04-26] Now requires -warn-invalid-bool
+- Wp [2019-04-26] Removed option -wp-bool-range
+- Wp [2019-04-24] Support for Why3 1.* and Coq 8.{7-9}
+- Wp [2019-02-26] Support for @check ACSL annotations
+- WP [2018-02-16] Filter out some variables from separation
+- TIP [2018-02-15] Extend bitwise-eq auto-strategy on hypotheses
+- TIP [2018-02-15] Fix wrong reconciliation of sub-scripts during replay
+- Wp [2018-02-15] Better naming convention, consistent with report-classify
+- WP [2019-02-05] Auto filter properties with name "no_wp:"
+- Wp [2019-01-28] Now -wp-dynamic is set by default (annotation @calls)
+- Wp [2019-01-28] New floating-point model
+- Wp [2018-01-18] Auto-Search mode, see -wp-auto
+- TIP [2018-01-18] Auto-Search mode from the GUI
+- TIP [2018-01-18] New Strategies for bitwise and congruence operations
+- TIP [2017-12-17] Fix bug that makes the TIP wrongly reuse previous results
+- Wp [2017-12-17] Option -wp-print-separation changed into -wp-warn-separation
+- Wp [2017-12-17] Option -wp-unfold-assigns for proving assigns of aggregates field by field
+- TIP [2017-04-25] New tactical Congruence (divisions and products)
+- Qed [2017-10-30] Extends simplifications for lsl,lsr and div
+- Wp [2017-10-27] Fix soundness bug when assigning non-valid ranges
+- Qed [2017-10-27] New simplifications for validity and ranges
+- TIP [2017-10-27] New tacticals for validity and ranges
######################
Plugin WP 18.0 (Argon)
######################
-- Wp [2018/10/25] Added support for ACSL \offset construct
-- Wp [2018/09/04] Option -wp-warn-separation changed into -wp-warn-memory-model
+- Wp [2018-10-25] Added support for ACSL \offset construct
+- Wp [2018-09-04] Option -wp-warn-separation changed into -wp-warn-memory-model
Adding memory model hypotheses related to pointer validity
-- Wp [2018/06/28] Use functional havoc instead of a predicate in Typed model
-- Qed [2018/06/28] Added builtin simplification on array operations
-- Wp [2018/06/20] Added more simplifications on list operations
-- Qed [2018/06/20] Added more simplifications for invertible functions
-- TIP [2018/06/07] Extends tactical 'Split' to distribution of qualitifiers
-
-#########################
-Plugin WP Sulfur-20171101
-#########################
-
-- Wp [2017/10/18] Support for LoopCurrent and LoopEntry
-- TIP [2017/04/25] Options -wp-time-{extra|margin} for more stability
--* Gui [2017/04/25] Fixed bug when running prover from the TIP
-- Wp [2017/04/25] Improved model and simplifications of logical shifts
-- Wp [2017/04/25] New simplification logic functions (-wp-reduce)
-- Wp [2017/04/25] New simplification of unused variables (-wp-parasite)
-- Wp [2017/04/25] New simplification for ground terms (-wp-ground)
-- Wp [2017/04/25] Option -wp-prenex to normalize nested binders
-- Wp [2017/04/25] Option -wp-overflows to add explicit assumptions
-- TIP [2017/04/25] New tactical Overflow (to cope with modulus)
-- TIP [2017/04/25] New tactical Ratio (divisions and products)
-- TIP [2017/04/25] New tactical Bitwised, BitRange and Shift
-- TIP [2017/04/25] New tactical Rewrite (two apply equalities)
-- Wp [2017/03/12] Reduction of equalities with logic functions
-- Wp [2017/03/12] More simplifications wrt integer domains
-
-###########################
-Plugin WP Chlorine-20180501
-###########################
-
-- WP [2018/03/08] Add the missing ACSL math builtins (see manual)
-- WP [2018/02/12] Experimental support for _Bool range (-wp-bool-range)
-- WP [2018/03/12] Better handling of \null and (void *)0L
-- WP [2018/02/16] Allow backtracking when using strategies (-wp-auto-backtrack)
-- WP [2018/02/16] Filter out some variables from separation
-- TIP [2018/02/15] Extend bitwise-eq auto-strategy on hypotheses
-- TIP [2018/02/15] Fix wrong reconciliation of sub-scripts during replay
-- WP [2018/01/15] Upgrade to Alt-Ergo 2.0.0
-- WP [2018/01/15] Upgrade to Coq 8.7.1
-- WP [2018/01/15] Upgrade to Why-3 0.88.3
-- Qed [2017/12/13] Transforms some quantifications into let constructs
-- WP [2018/01/18] Auto-Search mode, see -wp-auto
-- TIP [2018/01/18] Auto-Search mode from the GUI
-- TIP [2018/01/18] New Strategies for bitwise and congruence operations
-- TIP [2017/12/17] Fix bug that makes the TIP wrongly reuse previous results
-- WP [2017/12/17] Option -wp-print-separation changed into -wp-warn-separation
-- WP [2017/12/17] Option -wp-unfold-assigns for proving assigns of aggregates field by field
-- TIP [2017/04/25] New tactical Congruence (divisions and products)
-- Qed [2017/10/30] Extends simplifications for lsl,lsr and div
-- WP [2017/10/27] Fix soundness bug when assigning non-valid ranges
-- Qed [2017/10/27] New simplifications for validirt and ranges
-- TIP [2017/10/27] New tacticals for validity and ranges
-
-#########################
-Plugin WP Sulfur-20171101
-#########################
-
-- WP [2017/10/18] Support for LoopCurrent and LoopEntry
-- TIP [2017/04/25] Options -wp-time-{extra|margin} for more stability
--* Gui [2017/04/25] Fixed bug when running prover from the TIP
-- WP [2017/04/25] Improved model and simplifications of logical shifts
-- WP [2017/04/25] New simplification logic functions (-wp-reduce)
-- WP [2017/04/25] New simplification of unused variables (-wp-parasite)
-- WP [2017/04/25] New simplification for ground terms (-wp-ground)
-- WP [2017/04/25] Option -wp-prenex to normalize nested binders
-- WP [2017/04/25] Option -wp-overflows to add explicit assumptions
-- TIP [2017/04/25] New tactical Overflow (to cope with modulus)
-- TIP [2017/04/25] New tactical Ratio (divisions and products)
-- TIP [2017/04/25] New tactical Bitwised, BitRange and Shift
-- TIP [2017/04/25] New tactical Rewrite (two apply equalities)
-- WP [2017/03/12] Reduction of equalities with logic functions
-- WP [2017/03/12] More simplifications wrt integer domains
-
-#############################
-Plugin WP Phosphorus-20170501
-#############################
-
-- Qed [2017/12/13] Transforms some quantifications into let constructs
-- WP [2017/05/15] Extract inductive predicates as Inductive in Coq
--! WP [2017/03/24] Remove support for generalized invariants (-wp-invariants)
--o Ergo [2017/01/12] Update qualif tests to Alt-Ergo 1.30
-- Qed [2016/12/09] Add E_fun constructor for neutral and absorbent
-- WP [2016/12/07] Trivial simplification for truncate
-- WP [2016/12/07] Fix bug on negative 0x float constants
-- WP [2016/11/04] Improved comparison of logic compounds
-- WP [2016/11/04] Improved filtering (prevents loss of init clauses)
-- WP [2016/10/26] Generated HTML API (make wp-doc-api)
-- WP [2016/10/26] Extensible Proof Engine
--! WP [2016/10/11] Deprecated Dynamic API
-- WP [2016/09/20] Improved sequent simplifier
-- Qed [2016/09/02] Negation of forall/exists qualitifers
-- GUI [2016/08/26] Pretty-print of memory side effects
-- WP [2016/08/23] Fixed bug #2246 (unsound switch)
-- Gui [2016/07/23] Interactive Proof Engine
-- WP [2016/07/21] Improved Sequent API (Conditions)
-- WP [2016/05/26] Simplification of ACSL sequences
-- Qed [2016/05/17] Mutualized type inference in Term
-- Qed [2016/04/12] Improved simplifiers
-- WP [2016/11/17] Warn against access to volatile l-values
-- WP [2016/11/17] Fix volatile access (see -wp-no-volatile)
-
-##########################
-Plugin WP Silicon-20161101
-##########################
-
-- WP [2016/04/08] Unified variable usage for all models
-- WP [2016/10/06] Simplification of arithmetics models
-- WP [2016/10/06] Use kernel options -warn-xxx in cint model
-- WP [2016/10/06] Use cint and cfloat models by default
-- WP [2016/10/06] Fix -wp-rte with respect to models and kernel options
-
-################################
-Plugin WP 1.0 Aluminium_20160502
-################################
-
-- Coq [2016/03/30] Fixed bug #2214 (coq realbase)
-- WP [2016/03/29] Support for why3 0.87 (and ide)
-- WP [2016/03/25] Support for Why3 0.86
-- WP [2016/03/25] Support for Coq 8.5
-- WP [2016/02/24] Support for Alt-Ergo 1.01
-- WP [2016/02/18] Fix behavior on ASM code
-- WP [2016/02/15] Now follows '-safe-arrays' when refining 'p+(..)'
-- WP [2016/02/02] Added support for ACSL let-predicate
--! WP [2016/01/15] Removed alias '-wp-log' (use '-wp-msg-key' instead)
-- WP [2015/12/16] Strict parsing of -wp-model (stop on error)
-- Caveat [2015/12/02] Separation Hypotheses with -wp-print-separation
-- WP [2015/11/13] Exported OCaml API via Wp.mli
-- WP [2015/11/24] Added support for built-in ACSL lists
-- WP [2015/11/19] New options to set prover commands
-- Coq [2015/11/19] Support for Proof General 4.3
+- Wp [2018-06-28] Use functional havoc instead of a predicate in Typed model
+- Qed [2018-06-28] Added builtin simplification on array operations
+- Wp [2018-06-20] Added more simplifications on list operations
+- Qed [2018-06-20] Added more simplifications for invertible functions
+- TIP [2018-06-07] Extends tactical 'Split' to distribution of qualitifiers
+
+##################################
+Plugin WP 17.0 (Chlorine-20180501)
+##################################
+
+- WP [2018-03-08] Add the missing ACSL math builtins (see manual)
+- WP [2018-02-12] Experimental support for _Bool range (-wp-bool-range)
+- WP [2018-03-12] Better handling of \null and (void *)0L
+- WP [2018-02-16] Allow backtracking when using strategies (-wp-auto-backtrack)
+- WP [2018-02-16] Filter out some variables from separation
+- TIP [2018-02-15] Extend bitwise-eq auto-strategy on hypotheses
+- TIP [2018-02-15] Fix wrong reconciliation of sub-scripts during replay
+- WP [2018-01-15] Upgrade to Alt-Ergo 2.0.0
+- WP [2018-01-15] Upgrade to Coq 8.7.1
+- WP [2018-01-15] Upgrade to Why-3 0.88.3
+- Qed [2017-12-13] Transforms some quantifications into let constructs
+- WP [2018-01-18] Auto-Search mode, see -wp-auto
+- TIP [2018-01-18] Auto-Search mode from the GUI
+- TIP [2018-01-18] New Strategies for bitwise and congruence operations
+- TIP [2017-12-17] Fix bug that makes the TIP wrongly reuse previous results
+- WP [2017-12-17] Option -wp-print-separation changed into -wp-warn-separation
+- WP [2017-12-17] Option -wp-unfold-assigns for proving assigns of aggregates field by field
+- TIP [2017-04-25] New tactical Congruence (divisions and products)
+- Qed [2017-10-30] Extends simplifications for lsl,lsr and div
+- WP [2017-10-27] Fix soundness bug when assigning non-valid ranges
+- Qed [2017-10-27] New simplifications for validirt and ranges
+- TIP [2017-10-27] New tacticals for validity and ranges
################################
-Plugin WP 0.9 Magnesium_20151002
+Plugin WP 16.0 (Sulfur-20171101)
################################
-- WP [2015/09/02] Added support for float-classification.
+- WP [2017-10-18] Support for LoopCurrent and LoopEntry
+- TIP [2017-04-25] Options -wp-time-{extra|margin} for more stability
+-* Gui [2017-04-25] Fixed bug when running prover from the TIP
+- WP [2017-04-25] Improved model and simplifications of logical shifts
+- WP [2017-04-25] New simplification logic functions (-wp-reduce)
+- WP [2017-04-25] New simplification of unused variables (-wp-parasite)
+- WP [2017-04-25] New simplification for ground terms (-wp-ground)
+- WP [2017-04-25] Option -wp-prenex to normalize nested binders
+- WP [2017-04-25] Option -wp-overflows to add explicit assumptions
+- TIP [2017-04-25] New tactical Overflow (to cope with modulus)
+- TIP [2017-04-25] New tactical Ratio (divisions and products)
+- TIP [2017-04-25] New tactical Bitwised, BitRange and Shift
+- TIP [2017-04-25] New tactical Rewrite (two apply equalities)
+- WP [2017-03-12] Reduction of equalities with logic functions
+- WP [2017-03-12] More simplifications wrt integer domains
+
+####################################
+Plugin WP 15.0 (Phosphorus-20170501)
+####################################
+
+- Qed [2017-12-13] Transforms some quantifications into let constructs
+- WP [2017-05-15] Extract inductive predicates as Inductive in Coq
+-! WP [2017-03-24] Remove support for generalized invariants (-wp-invariants)
+-o Ergo [2017-01-12] Update qualif tests to Alt-Ergo 1.30
+- Qed [2016-12-09] Add E_fun constructor for neutral and absorbent
+- WP [2016-12-07] Trivial simplification for truncate
+- WP [2016-12-07] Fix bug on negative 0x float constants
+- WP [2016-11-04] Improved comparison of logic compounds
+- WP [2016-11-04] Improved filtering (prevents loss of init clauses)
+- WP [2016-10-26] Generated HTML API (make wp-doc-api)
+- WP [2016-10-26] Extensible Proof Engine
+-! WP [2016-10-11] Deprecated Dynamic API
+- WP [2016-09-20] Improved sequent simplifier
+- Qed [2016-09-02] Negation of forall-exists qualitifers
+- GUI [2016-08-26] Pretty-print of memory side effects
+- WP [2016-08-23] Fixed bug #2246 (unsound switch)
+- Gui [2016-07-23] Interactive Proof Engine
+- WP [2016-07-21] Improved Sequent API (Conditions)
+- WP [2016-05-26] Simplification of ACSL sequences
+- Qed [2016-05-17] Mutualized type inference in Term
+- Qed [2016-04-12] Improved simplifiers
+- WP [2016-11-17] Warn against access to volatile l-values
+- WP [2016-11-17] Fix volatile access (see -wp-no-volatile)
+
+#################################
+Plugin WP 14.0 (Silicon-20161101)
+#################################
+
+- WP [2016-04-08] Unified variable usage for all models
+- WP [2016-10-06] Simplification of arithmetics models
+- WP [2016-10-06] Use kernel options -warn-xxx in cint model
+- WP [2016-10-06] Use cint and cfloat models by default
+- WP [2016-10-06] Fix -wp-rte with respect to models and kernel options
+
+##################################
+Plugin WP 1.0 (Aluminium_20160502)
+##################################
+
+- Coq [2016-03-30] Fixed bug #2214 (coq realbase)
+- WP [2016-03-29] Support for why3 0.87 (and ide)
+- WP [2016-03-25] Support for Why3 0.86
+- WP [2016-03-25] Support for Coq 8.5
+- WP [2016-02-24] Support for Alt-Ergo 1.01
+- WP [2016-02-18] Fix behavior on ASM code
+- WP [2016-02-15] Now follows '-safe-arrays' when refining 'p+(..)'
+- WP [2016-02-02] Added support for ACSL let-predicate
+-! WP [2016-01-15] Removed alias '-wp-log' (use '-wp-msg-key' instead)
+- WP [2015-12-16] Strict parsing of -wp-model (stop on error)
+- Caveat [2015-12-02] Separation Hypotheses with -wp-print-separation
+- WP [2015-11-13] Exported OCaml API via Wp.mli
+- WP [2015-11-24] Added support for built-in ACSL lists
+- WP [2015-11-19] New options to set prover commands
+- Coq [2015-11-19] Support for Proof General 4.3
+
+##################################
+Plugin WP 0.9 (Magnesium_20151002)
+##################################
+
+- WP [2015-09-02] Added support for float-classification.
(\is_NaN, \is_finite, \is_infinite, \is_plus_infinity, \is_minus_infinity).
--* WP [2015/09/02] Fixed bug #2082 (crash with \is_infinite).
--* WP [2015/08/19] Fixed bug #2040 (wrong label Here in assumes).
--* WP [2015/08/18] Fixed bug #2110 (wrong premisses for structs assigns).
--* WP [2015/08/18] Fixed bug #2141 (incorrect simplification of 'x%1').
--* WP [2015/08/18] Fixed bug #2144 (lost \result after explicit assignment).
--* WP [2015/06/29] Fixed bug #2078 (ill typed PO with void*).
--* WP [2015/06/29] Fixed bug #2127 (unsigned inequality).
--* WP [2015/06/29] Fixed bug #2126 (0-shift rewriting).
--* WP [2015/05/20] Fixed bug #1683 (multiply reported Qed proofs).
--* WP [2015/03/20] Fixed bug #2079 (incorrect pointer arithmetics).
-- WP [2015/02/28] Handle global constants (-wp-init-const).
-- WP [2015/02/28] Quiet output on TTY (see -tty kernel option).
-- WP [2015/02/28] Added solver mean time to console output.
--* Hoare [2015/02/28] Fixed incorrect partial assignments in compound objects.
-- WP [2015/02/28] Refactoring of compound objects modeling.
-- Qed [2015/02/28] Fold constant expressions in goals.
-- Qed [2015/02/28] More simplifications on strict inequalities.
-- Qed [2015/02/28] More aggressive filtering and pruning (-wp-filter).
-- Qed [2015/02/28] Aggressive ite-lifting.
-- Qed [2015/02/28] Automatic introduction of existentials.
--! Coq [2015/02/28] Inductive if-then-else construct.
-- WP [2015/02/28] -wp-simplify-type remove some most type constraints (sound, incomplete).
-- WP [2015/02/28] -wp-simplify-forall of quantifier guards (unsound).
-- Qed [2015/02/28] Factorization of core equalities (-wp-core).
-- WP [2015/02/28] Improved -wp-check mode.
--* WP [2015/02/28] Fixed bool-prop conversions.
-- WP [2015/02/28] Summarize initializers (-wp-init-summarize-array).
-- WP [2015/02/28] Simplifications of 'is_cint' with quantifiers.
-- Caveat [2015/02/28] New 'Caveat' memory model.
-- Typed [2015/02/28] Named shift operators (better triggers).
-- WP [2015/02/28] New integer model '+rg'.
--* WP [2015/02/28] Fixed bug #1683 (duplicate Qed results).
--* WP [2015/02/28] Improved typing for alt-ergo let-bindings.
--* WP [2015/02/28] Fix sharing bug in proof obligation output.
-- Report [2015/02/28] Support for CVC4 reporting.
--* WP [2015/02/28] Fix bugs with -wp-extern-arrays.
-- WP [2015/02/28] More lemmas for bitwise operations.
-- WP [2015/02/28] Options -wp-*-vars to tune memory model detection.
--* WP [2015/02/18] Fixed bug #1785 (fixed pre-condition with Clang).
-- WP [2015/01/27] Support for \subset.
-- WP [2014/09/24] Now accept patterns in drivers.
--* WP [2014/09/15] Fixed bug #1828 (separation of locals/formals/heap).
+-* WP [2015-09-02] Fixed bug #2082 (crash with \is_infinite).
+-* WP [2015-08-19] Fixed bug #2040 (wrong label Here in assumes).
+-* WP [2015-08-18] Fixed bug #2110 (wrong premisses for structs assigns).
+-* WP [2015-08-18] Fixed bug #2141 (incorrect simplification of 'x%1').
+-* WP [2015-08-18] Fixed bug #2144 (lost \result after explicit assignment).
+-* WP [2015-06-29] Fixed bug #2078 (ill typed PO with void*).
+-* WP [2015-06-29] Fixed bug #2127 (unsigned inequality).
+-* WP [2015-06-29] Fixed bug #2126 (0-shift rewriting).
+-* WP [2015-05-20] Fixed bug #1683 (multiply reported Qed proofs).
+-* WP [2015-03-20] Fixed bug #2079 (incorrect pointer arithmetics).
+- WP [2015-02-28] Handle global constants (-wp-init-const).
+- WP [2015-02-28] Quiet output on TTY (see -tty kernel option).
+- WP [2015-02-28] Added solver mean time to console output.
+-* Hoare [2015-02-28] Fixed incorrect partial assignments in compound objects.
+- WP [2015-02-28] Refactoring of compound objects modeling.
+- Qed [2015-02-28] Fold constant expressions in goals.
+- Qed [2015-02-28] More simplifications on strict inequalities.
+- Qed [2015-02-28] More aggressive filtering and pruning (-wp-filter).
+- Qed [2015-02-28] Aggressive ite-lifting.
+- Qed [2015-02-28] Automatic introduction of existentials.
+-! Coq [2015-02-28] Inductive if-then-else construct.
+- WP [2015-02-28] -wp-simplify-type remove some most type constraints (sound, incomplete).
+- WP [2015-02-28] -wp-simplify-forall of quantifier guards (unsound).
+- Qed [2015-02-28] Factorization of core equalities (-wp-core).
+- WP [2015-02-28] Improved -wp-check mode.
+-* WP [2015-02-28] Fixed bool-prop conversions.
+- WP [2015-02-28] Summarize initializers (-wp-init-summarize-array).
+- WP [2015-02-28] Simplifications of 'is_cint' with quantifiers.
+- Caveat [2015-02-28] New 'Caveat' memory model.
+- Typed [2015-02-28] Named shift operators (better triggers).
+- WP [2015-02-28] New integer model '+rg'.
+-* WP [2015-02-28] Fixed bug #1683 (duplicate Qed results).
+-* WP [2015-02-28] Improved typing for alt-ergo let-bindings.
+-* WP [2015-02-28] Fix sharing bug in proof obligation output.
+- Report [2015-02-28] Support for CVC4 reporting.
+-* WP [2015-02-28] Fix bugs with -wp-extern-arrays.
+- WP [2015-02-28] More lemmas for bitwise operations.
+- WP [2015-02-28] Options -wp-*-vars to tune memory model detection.
+-* WP [2015-02-18] Fixed bug #1785 (fixed pre-condition with Clang).
+- WP [2015-01-27] Support for \subset.
+- WP [2014-09-24] Now accept patterns in drivers.
+-* WP [2014-09-15] Fixed bug #1828 (separation of locals/formals/heap).
-#############################
-Plugin WP 0.8 Sodium_20150201
-#############################
+###############################
+Plugin WP 0.8 (Sodium_20150201)
+###############################
-- WP [2014/09/05] Drivers for min/max.
-- Typed [2014/09/04] Simplification of assigns and separated.
--* Gui [2014/09/04] Fixed bug #1688 (recover results from cmdline).
--! WP [2014/07/09] Next to the new way the kernel handles command line
+- WP [2014-09-05] Drivers for min/max.
+- Typed [2014-09-04] Simplification of assigns and separated.
+-* Gui [2014-09-04] Fixed bug #1688 (recover results from cmdline).
+-! WP [2014-07-09] Next to the new way the kernel handles command line
options, -wp-include +dir has to be replaced by -wp-include ++dir.
Forward and backward compatibilities are broken.
-- WP [2014/06/11] Some improvements on bitwise operators.
-- Cmd [2014/05/22] Added option -wp-filename-truncation to truncate
+- WP [2014-06-11] Some improvements on bitwise operators.
+- Cmd [2014-05-22] Added option -wp-filename-truncation to truncate
proof obligation filenames.
-###########################
-Plugin WP 0.8 Neon_20140301
-###########################
+#############################
+Plugin WP 0.8 (Neon_20140301)
+#############################
-- Gui [2014/01/30] Edition of current proof script (right-click).
-- Gui [2014/01/30] Consistent icons with status.
-- Driver [2014/01/30] Refactoring of prover external libraries.
+- Gui [2014-01-30] Edition of current proof script (right-click).
+- Gui [2014-01-30] Consistent icons with status.
+- Driver [2014-01-30] Refactoring of prover external libraries.
(consult driver section in manual).
--* WP [2014/01/16] Important bug-fix in CFG (missing hyps in goals).
--* WP [2013/12/11] Major speed-up for huge functions.
-- WP [2014/01/30] Many improvements on reals and floats.
-- WP [2014/01/30] Many improvements on bitwise operators.
-- WP [2014/01/30] Better integration with Why-3 and Coq.
-- WP [2013/12/09] Clever assigns everything with formals and locals.
-- WP [2013/11/26] More type constraints in typed memory model.
-
-###############################
-Plugin WP 0.7 Fluorine_20130501
-###############################
-
--* Typed [2013/05/23] Better trigger generation for arrays with Alt-Ergo.
--* Provers [2013/05/23] Fixed various bugs with drivers and provers.
--* WP [2013/05/23] Fixed various bugs on floats.
--* Typed [2013/05/23] Fixed bug on address differences and offsets.
-
-###############################
-Plugin WP 0.7 Fluorine_20130401
-###############################
-
--* Makefile [2013/04/17] Fixed bug #1385 about ocamllex.opt.
--! Cmd [2013/04/15] Removed now useless options -wp-huge, -wp-dot,
+-* WP [2014-01-16] Important bug-fix in CFG (missing hyps in goals).
+-* WP [2013-12-11] Major speed-up for huge functions.
+- WP [2014-01-30] Many improvements on reals and floats.
+- WP [2014-01-30] Many improvements on bitwise operators.
+- WP [2014-01-30] Better integration with Why-3 and Coq.
+- WP [2013-12-09] Clever assigns everything with formals and locals.
+- WP [2013-11-26] More type constraints in typed memory model.
+
+#################################
+Plugin WP 0.7 (Fluorine_20130501)
+#################################
+
+-* Typed [2013-05-23] Better trigger generation for arrays with Alt-Ergo.
+-* Provers [2013-05-23] Fixed various bugs with drivers and provers.
+-* WP [2013-05-23] Fixed various bugs on floats.
+-* Typed [2013-05-23] Fixed bug on address differences and offsets.
+
+#################################
+Plugin WP 0.7 (Fluorine_20130401)
+#################################
+
+-* Makefile [2013-04-17] Fixed bug #1385 about ocamllex.opt.
+-! Cmd [2013-04-15] Removed now useless options -wp-huge, -wp-dot,
-wp-trace.
-- Cmd [2013/04/15] Added option -wp-skip-fct to exclude functions.
-- Cmd [2013/04/15] Using -wp-prover instead of -wp-proof
+- Cmd [2013-04-15] Added option -wp-skip-fct to exclude functions.
+- Cmd [2013-04-15] Using -wp-prover instead of -wp-proof
(kept for compatibility).
-- Gui [2013/04/15] New Why3 provers selection, added -wp-detect to
+- Gui [2013-04-15] New Why3 provers selection, added -wp-detect to
force detection.
-- WP [2013/02/29] Added support for string literals (-wp-literals).
-- WP [2013/02/01] New simplification engine (specific options).
-- WP [2013/02/01] New interface to model selection (unique
+- WP [2013-02-29] Added support for string literals (-wp-literals).
+- WP [2013-02-01] New simplification engine (specific options).
+- WP [2013-02-01] New interface to model selection (unique
-wp-model option).
-- WP [2013/02/01] Experimental float and machine-integer models.
-- WP [2013/02/01] 'Store' and 'Runtime' models abandoned.
-- WP [2013/01/09] 'Typed' becomes the default model.
-- Why3 [2012/12/18] Why3 output (-wp-proof why3:xxx).
-- Typed [2012/10/23] Extensions of Typed model (unsafe-casts).
-- WP [2012/10/09] Drivers for linking ACSL symbols to external
+- WP [2013-02-01] Experimental float and machine-integer models.
+- WP [2013-02-01] 'Store' and 'Runtime' models abandoned.
+- WP [2013-01-09] 'Typed' becomes the default model.
+- Why3 [2012-12-18] Why3 output (-wp-proof why3:xxx).
+- Typed [2012-10-23] Extensions of Typed model (unsafe-casts).
+- WP [2012-10-09] Drivers for linking ACSL symbols to external
libs (-wp-driver).
-#############################
-Plugin WP 0.6 Oxygen_20120901
-#############################
+###############################
+Plugin WP 0.6 (Oxygen_20120901)
+###############################
-- WP [2012/09/14] Experimental simplifier with new 'Typed' model
+- WP [2012-09-14] Experimental simplifier with new 'Typed' model
(see manual).
-o! WP [2012/09/05] Enhanced Ocaml API (see manual). Old bindings
+o! WP [2012-09-05] Enhanced Ocaml API (see manual). Old bindings
are preserved, but now emit a deprecated warning.
--* WP [2012/07/31] Fixed issue about -ulevel option (bug #1244).
-- WP [2012/06/30] Truncating too long log filenames.
-- WP [2012/06/20] Enhanced statistics for -wp-report (see manual).
--* Coq [2012/05/22] Better translation in Coq for floats and reals
+-* WP [2012-07-31] Fixed issue about -ulevel option (bug #1244).
+- WP [2012-06-30] Truncating too long log filenames.
+- WP [2012-06-20] Enhanced statistics for -wp-report (see manual).
+-* Coq [2012-05-22] Better translation in Coq for floats and reals
(fixed bugs #1174 and #1176).
-- Gui [2012/05/15] Graphical version of Alt-Ergo (altgr-ergo) can be
+- Gui [2012-05-15] Graphical version of Alt-Ergo (altgr-ergo) can be
launched from the 'Proof Obligation Panel'.
-- Cmd [2012/03/15] Extended selection language: -wp-prop [+|-][@]id
+- Cmd [2012-03-15] Extended selection language: -wp-prop [+|-][@]id
to add or remove property category or name.
-- WP [2012/03/06] Better elimination of let constructs for -wp-norm Eqs
+- WP [2012-03-06] Better elimination of let constructs for -wp-norm Eqs
option.
-- WP [2012/02/08] Limited support for triggers in axioms and lemmas.
-- Cmd [2012/02/03] Extended support for external libraries:
+- WP [2012-02-08] Limited support for triggers in axioms and lemmas.
+- Cmd [2012-02-03] Extended support for external libraries:
Options -wp-coq-lib, -wp-why-lib and now -wp-alt-ergo-lib.
-###############################
-Plugin WP 0.5 Nitrogen_20111001
-###############################
+#################################
+Plugin WP 0.5 (Nitrogen_20111001)
+#################################
-+* Store [2012/01/03] Adding guard for 'fresh' axiomatization in Store.
-+ WP [2011/12/23] Timing.
-- Gui [2011/12/19] Changes into Gui panel.
-- Cmd [2011/12/16] Adding support for reporting with option: -wp-report.
-+* WP [2011/11/25] Fixed bug #!1020 on arbitrary invariants.
-- Cmd [2011/11/22] Adding support for external proof libraries.
++* Store [2012-01-03] Adding guard for 'fresh' axiomatization in Store.
++ WP [2011-12-23] Timing.
+- Gui [2011-12-19] Changes into Gui panel.
+- Cmd [2011-12-16] Adding support for reporting with option: -wp-report.
++* WP [2011-11-25] Fixed bug #!1020 on arbitrary invariants.
+- Cmd [2011-11-22] Adding support for external proof libraries.
See options -wp-include, -wp-tactic, -wp-coq-lib and -wp-why-lib.
-- Cmd [2011/11/21] Adding support for multi-provers in command line.
+- Cmd [2011-11-21] Adding support for multi-provers in command line.
-###############################
-Plugin WP 0.4 Nitrogen_20111001
-###############################
+#################################
+Plugin WP 0.4 (Nitrogen_20111001)
+#################################
-- WP [2011/10/24] Further improvement for proof of assigns clauses.
-- WP [2011/10/14] A warning is now emitted for missing assigns clauses.
-+* WP [2011/09/30] Fixed bug #!572 for logic declaration without
+- WP [2011-10-24] Further improvement for proof of assigns clauses.
+- WP [2011-10-14] A warning is now emitted for missing assigns clauses.
++* WP [2011-09-30] Fixed bug #!572 for logic declaration without
'reads' clause.
-+* WP [2011/09/22] Fixed bug #!970 for labels that may escape the
++* WP [2011-09-22] Fixed bug #!970 for labels that may escape the
control flow.
-+* WP [2011/09/07] Fixed bug #!943 on translation of reals and floats
-- Cmd [2011/08/25] Optimization of arguments passing by reference
++* WP [2011-09-07] Fixed bug #!943 on translation of reals and floats
+- Cmd [2011-08-25] Optimization of arguments passing by reference
with option: -wp-byreference.
-- WP [2011/09/15] Improvements of conversion between C-integers
+- WP [2011-09-15] Improvements of conversion between C-integers
and Z-integers.
-- WP [2011/07/22] Optimization of arguments passing by reference.
-- WP [2011/07/22] Print of formula change.
-- Gui [2011/06/29] Feedback for proof of preconditions at call sites.
-- Gui [2011/06/29] New menu options to prove preconditions at one
+- WP [2011-07-22] Optimization of arguments passing by reference.
+- WP [2011-07-22] Print of formula change.
+- Gui [2011-06-29] Feedback for proof of preconditions at call sites.
+- Gui [2011-06-29] New menu options to prove preconditions at one
or all call sites.
-- Cmd [2011/06/17] Added option -wp-proof-trace to obtain more
+- Cmd [2011-06-17] Added option -wp-proof-trace to obtain more
informations from provers when available (option 'Trace' in GUI).
--! Ergo [2011/06/17] Alt-Ergo is always used with builtin arrays.
+-! Ergo [2011-06-17] Alt-Ergo is always used with builtin arrays.
Removed option -wp-arrays.
-- Vampire [2011/06/10] Support for Vampire as back-end prover.
--* WP [2011/06/10] In some cases, a proof attempt could silently
+- Vampire [2011-06-10] Support for Vampire as back-end prover.
+-* WP [2011-06-10] In some cases, a proof attempt could silently
failed. It is now properly reported.
-- Gui [2011/06/07] Default output directory is set to
- <home>/.frama-c-wp in Gui.
-- Gui [2011/06/07] Enhancement of Proof-Obligation panel.
--! WP [2011/05/20] Translation of axioms with labels
+- Gui [2011-06-07] Default output directory is set to
+ <home>-.frama-c-wp in Gui.
+- Gui [2011-06-07] Enhancement of Proof-Obligation panel.
+-! WP [2011-05-20] Translation of axioms with labels
(removed option -wp-axioms).
-+ Caveat [2011/05/19] Suppression of legacy Caveat model.
-- Hoare [2011/05/19] New Hoare model
++ Caveat [2011-05-19] Suppression of legacy Caveat model.
+- Hoare [2011-05-19] New Hoare model
(now implemented on top of logic variables).
-- WP [2011/05/19] Handling partial initializers in C global variables.
-- Cmd [2011/05/17] New engine to compute proof obligations for
+- WP [2011-05-19] Handling partial initializers in C global variables.
+- Cmd [2011-05-17] New engine to compute proof obligations for
arbitrary invariants. See option -wp-invariants.
--! Ergo [2011/05/17] Alt-Ergo 0.93 now required.
--! Gui [2011/05/17] Removed 'Refresh' button from WP panel.
-+* Gui [2011/05/17] Fixed bug #!706 : property status not refreshed.
-+* Gui [2011/05/17] Fixed bug #!707 : unexpected run of wp provers
+-! Ergo [2011-05-17] Alt-Ergo 0.93 now required.
+-! Gui [2011-05-17] Removed 'Refresh' button from WP panel.
++* Gui [2011-05-17] Fixed bug #!706 : property status not refreshed.
++* Gui [2011-05-17] Fixed bug #!707 : unexpected run of wp provers
after -then.
-+* WP [2011/05/02] Fixed bug #!708 (missing definitions in
++* WP [2011-05-02] Fixed bug #!708 (missing definitions in
environments).
-- WP [2011/04/29] Alt-Ergo is now selected (and run) by default.
--* WP [2011/04/29] Fixed problems with -wp-out <dir>.
-- WP [2011/04/21] Better representation of records and unions in logic.
-- WP [2011/04/21] No more logic generic pointers. Pointer arithmetics
+- WP [2011-04-29] Alt-Ergo is now selected (and run) by default.
+-* WP [2011-04-29] Fixed problems with -wp-out <dir>.
+- WP [2011-04-21] Better representation of records and unions in logic.
+- WP [2011-04-21] No more logic generic pointers. Pointer arithmetics
moved to memory models.
--* Store [2011/04/21] Better representation of pointers (issue #796).
--* Gui [2011/04/15] Fixed bug on PO status (wrong PO identification).
--* Gui [2011/04/13] Fixed bug #711 (cyclic dependencies).
+-* Store [2011-04-21] Better representation of pointers (issue #796).
+-* Gui [2011-04-15] Fixed bug on PO status (wrong PO identification).
+-* Gui [2011-04-13] Fixed bug #711 (cyclic dependencies).
-#############################
-Plugin WP 0.3 Carbon_20110201
-#############################
+###############################
+Plugin WP 0.3 (Carbon_20110201)
+###############################
--* Coq [2011/04/08] Fixed bug #740 for Coq on Windows.
+-* Coq [2011-04-08] Fixed bug #740 for Coq on Windows.
WP now uses directly coqtop -compile instead of coqc.
-- Runtime [2011/04/01] Optimization of effect-assigns.
--* Store [2011/03/30] Fixed bug #766 about offsets in assigns.
-- Cmd [2011/03/23] Adding version in -wp-help.
-+* WP [2011/03/10] Proof of requires of the main entry point (bug #675).
-- Cmd [2011/01/31] Option -wp-warnings to display additional
+- Runtime [2011-04-01] Optimization of effect-assigns.
+-* Store [2011-03-30] Fixed bug #766 about offsets in assigns.
+- Cmd [2011-03-23] Adding version in -wp-help.
++* WP [2011-03-10] Proof of requires of the main entry point (bug #675).
+- Cmd [2011-01-31] Option -wp-warnings to display additional
informations for 'Stronger' and 'Degenerated' goals.
-- WP [2011/01/24] New spliting algorithm. See option -wp-split.
+- WP [2011-01-24] New spliting algorithm. See option -wp-split.
Option -wp-split-dim <n> to limit spliting up to 2**n sub-goals.
-- WP [2011/01/24] When -rte-precond is not used,
+- WP [2011-01-24] When -rte-precond is not used,
wp generates a separate proof obligation for each call site.
-- Cmd [2011/01/20] Options -wp-status-xxx to refine goal selection
-- Cmd [2011/01/19] Clarification of -save/-then effect on WP
--* Gui [2011/01/10] Fixed incorrect property status refresh in the GUI.
--* Coq [2011/01/04] Fixed bug #702 on Coq output with large integers.
--* WP [2011/03/10] Proof of requires of the main entry point (bug #675).
+- Cmd [2011-01-20] Options -wp-status-xxx to refine goal selection
+- Cmd [2011-01-19] Clarification of -save/-then effect on WP
+-* Gui [2011-01-10] Fixed incorrect property status refresh in the GUI.
+-* Coq [2011-01-04] Fixed bug #702 on Coq output with large integers.
+-* WP [2011-03-10] Proof of requires of the main entry point (bug #675).
-#############################
-Plugin WP 0.2 Carbon_20101202
-#############################
+###############################
+Plugin WP 0.2 (Carbon_20101202)
+###############################
--* Coq [2010/12/16] Fixed bug #639: no more compilation to shared
+-* Coq [2010-12-16] Fixed bug #639: no more compilation to shared
directory.
-- Gui [2010/12/16] Accessibility of all provers from gui.
+- Gui [2010-12-16] Accessibility of all provers from gui.
-#############################
-Plugin WP 0.1 Carbon_20101201
-#############################
+###############################
+Plugin WP 0.1 (Carbon_20101201)
+###############################
-- WP [2010/12/06] New WP plugin.
+- WP [2010-12-06] New WP plugin.
#############################