-
Allan Blanchard authoredAllan Blanchard authored
To find the state of this project's repository at the time of any of these versions, check out the tags.
Changelog 30.15 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
###############################################################################
########################
Plugin WP <next-release>
########################
- WP [2022-02-02] New option -wp-smoke-dead-local-init, smoke tests on
local variables initialization
- WP [2022-01-25] Removed deprecated "native:coq" prover
- WP [2022-01-25] Removed deprecated "native:alt-ergo" prover
- WP [2022-01-10] Supported general variant measure
- WP [2022-01-10] Supported decreases clause
- TIP [2022-01-10] New tactic Mod-Mask: rewrite bitmask into/from modulo
- TIP [2022-01-05] New tactic Clear: remove hypothesis
-* WP [2022-01-05] Fixed loop invariant order
- WP [2022-01-05] Weakened loop invariant verification (in particular
for check loop invariant)
- TIP [2021-11-30] Extended Split tactic: can split in hypotheses, can
split conjunctions into multiple hypotheses.
- WP [2021-11-08] Removed legacy WP engine and option -wp-legacy
#########################
Plugin WP 24.0 (Chromium)
#########################
- WP [2021-10-25] Removes -wp-overflows option (unsound)
- WP [2021-06-11] Adds an experimental support of "terminates" clauses.
Adds the options -wp-declaration-terminate and
-wp-frama-c-stdlib to claim that external functions
terminates.
Adds -wp-definitions-terminate option to claim that
defined function terminates.
Adds -wp-variant-with-terminates to verify loop
variants under the termination hypothesis.
- WP [2021-06-01] -wp-smoke-tests detects incoherent assumes when no
requires are specified, can be disabled with new
option -wp-smoke-dead-assumes
- TIP [2021-05-31] Generalized Overflow tactic
#########################
Plugin WP 23.1 (Vanadium)
#########################
- WP [2021-07-15] Fix a crash related to opaque structures memory typing
#########################
Plugin WP 23.0 (Vanadium)
#########################
- WP [2021-03-01] Section « Limitation & Roadmap » added to the WP manual.- WP [2021-03-01] New internal WP engine, fixing many issues related to
control flow graph and local variable scoping.
Support for stmt contracts has been removed.
Support for looping gotos has been removed.
Altough unsound, the legacy engine is still
accessible via -wp-legacy option.
- WP [2021-01-25] Improved -wp-unfold-assigns <depth>
Now recursively applies to all compounds
-* WP [2020-01-20] Fixes opaque structures handling
- TIP [2020-11-06] New tactic: Sequence unrolling
- TIP [2020-11-05] New tactic: Induction
- WP [2020-11-04] Removed option -wp-bits (now always enabled)
#########################
Plugin WP 22.0 (Titanium)
#########################
- WP [2020-10-14] New warning "pedantic-assigns". WP needs precise
'assigns ... \from ...' specification about out
pointers (\result and assigned pointers) to generate
precise proof hypotheses.
- WP [2020-10-14] Hypotheses: out pointers (\result + written pointers)
- WP [2020-10-07] New tactic Bit-Test range
- WP [2020-09-21] Added support for Why3 interactive prover (Coq)
- WP [2020-09-21] Added support for Why3 Coq interactive prover
- WP [2020-09-21] New option -wp-interactive <mode>
- WP [2020-09-21] New option -wp-interactive-timeout <seconds>
- WP [2020-09-17] New experimental option: -wp-check-memory-model
Insert function contracts for model hypotheses
- WP [2020-09-17] Hypotheses: assigned memory locations
- WP [2020-09-11] Support for generalized @check ACSL annotations
- WP [2020-07-06] Removed debug keys "no-xxx-info" (subsumed by "shell")
- WP [2020-07-06] Option -wp-cache-env now defaults to false
- WP [2020-07-06] New option -wp-cache-print
- WP [2020-06-12] Supports the \initialized ACSL predicate
#########################
Plugin WP 21.1 (Scandium)
#########################
-* WP [2020-06-23] Fixes Coq region function
-* WP [2020-06-23] Fixes MemTyped structure loader for wp-rte
#########################
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
##########################
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
##########################
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 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 16.0 (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 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).
###############################
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.
#############################