-
Loïc Correnson authoredLoïc Correnson authored
To find the state of this project's repository at the time of any of these versions, check out the tags.
Changelog 23.34 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:
# Cmd: command line interface
# Gui: graphical user interface
# Makefile: Makefile
# WP: proof obligation calculus
# <Model>: memory model
# <Prover>: prover
###############################################################################
- WP [2019/09/12] New cache mechanism for why3 provers, see -wp-cache option
- WP [2019/06/27] Improving Cint simplifier and quantifier introduction
o WP [2019/06/27] Using the new API of Qed
o Qed [2019/06/27] Changes into the API in order to get a more secure way to manipulate quantifiers and binding
- Qed [2019/05/09] Transforms some boolean quantifications into let constructs
##########################
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
######################
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
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
################################
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).
#############################
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
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
proof obligation filenames.
###########################
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.
(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-trace.
- 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
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-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
libs (-wp-driver).
#############################
Plugin WP 0.6 Oxygen_20120901
#############################
- WP [2012/09/14] Experimental simplifier with new 'Typed' model
(see manual).
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
(fixed bugs #1174 and #1176).
- 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
to add or remove property category or name.
- 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:
Options -wp-coq-lib, -wp-why-lib and now -wp-alt-ergo-lib.
###############################
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.
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.
###############################
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
'reads' clause.+* 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
with option: -wp-byreference.
- 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
or all call sites.
- 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.
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
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
(removed option -wp-axioms).
+ 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
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
after -then.
+* 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
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).
#############################
Plugin WP 0.3 Carbon_20110201
#############################
-* 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
informations for 'Stronger' and 'Degenerated' goals.
- 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 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).
#############################
Plugin WP 0.2 Carbon_20101202#############################
-* Coq [2010/12/16] Fixed bug #639: no more compilation to shared
directory.
- Gui [2010/12/16] Accessibility of all provers from gui.
#############################
Plugin WP 0.1 Carbon_20101201
#############################
- WP [2010/12/06] New WP plugin.
#############################