Skip to content
Snippets Groups Projects
Commit 90d99d6b authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[Changelog] better normalization and minor fixes

parent 694462ce
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Changelog
+ 6
− 6
View file @ 90d99d6b
......@@ -3505,11 +3505,11 @@ Open Source Release 4.1 (Beryllium-20090901)
-! Syntactic_callgraph [2009-08-27] New design of the callgraph in the GUI.
Frama-C now requires ocamlgraph 1.2.
- Logic "reads" clauses on logic functions and predicates, which
disappeared with the introduction of axiomatic blocks, have been
resurected. Beware that the semantics is slightly different
from before: see ACSL document for details. It is used to
automatically generate footprint axioms.
- Logic [2009-08-25]"reads" clauses on logic functions and predicates,
which disappeared with the introduction of axiomatic blocks,
have been ressurrected. Beware that the semantics is slightly
different from before: see ACSL document for details. It is used
to automatically generate footprint axioms.
- GUI [2009-08-18] Improved display of summary information when
selecting a file.
- Kernel [2009-08-05] New options -kernel-help, -kernel-verbose and
......@@ -3968,7 +3968,7 @@ Binary Release 1.0 (Hydrogen-20080302)
Open Source Release 1.0 (Hydrogen-20080301)
###########################################
- First release
- Kernel [2008-03-01] First release.
......
src/plugins/e-acsl/doc/Changelog
+ 13
− 14
View file @ 90d99d6b
......@@ -38,7 +38,6 @@ Plugin E-ACSL 21.0 (Scandium)
model analysis is running.
-* 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
of variables declared inside the body of switches.
- E-ACSL [2020-02-09] Improve verdict messages emitted by e_acsl_assert.
......@@ -146,7 +145,7 @@ Plugin E-ACSL 16.0 (Sulfur-20171101)
respective shadow spaces.
########################################
Plugin E-ACSL 15.0 (Phosphorus-20170515)
Plugin E-ACSL 15.0 (Phosphorus-20170501)
########################################
- runtime [2017-03-29] The (much more efficient) shadow memory model is
......@@ -173,9 +172,9 @@ Plugin E-ACSL 15.0 (Phosphorus-20170515)
operations in a few cases: the generated code might have
overflowed.
###########################
Plugin E-ACSL 0.8 (Silicon)
###########################
####################################
Plugin E-ACSL 0.8 (Silicon-20161101)
####################################
-* 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.
......@@ -211,9 +210,9 @@ Plugin E-ACSL 0.8 (Silicon)
initialization of tracked memory blocks in the E-ACSL
memory model library.
#############################
Plugin E-ACSL 0.6 (Magnesium)
#############################
######################################
Plugin E-ACSL 0.6 (Magnesium_20151002)
######################################
-* e-acsl-gcc [2016-01-22] Add an e-acsl-gcc.sh option allowing to skip
compilation of original sources.
......@@ -227,9 +226,9 @@ Plugin E-ACSL 0.6 (Magnesium)
-* 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_20150201)
###################################
- E-ACSL [2015-06-01] Support of \freeable. Thus illegal calls to
free (e.g. double free) are detected.
......@@ -245,9 +244,9 @@ 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_20140301)
###################################
-* E-ACSL [2014-08-05] Fix bug #1838 about memset.
-* E-ACSL [2014-08-05] Fix bug #1818 about initialization of globals.
......
src/plugins/wp/Changelog
+ 27
− 27
View file @ 90d99d6b
......@@ -24,33 +24,33 @@
Plugin WP 21.0 (Scandium)
#########################
- 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)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment