Changes in FramaC WP by Release


Release WP 0.5[Nitrogen 20111001]
WP  Gui
 [Gui] Changes into Gui panel.
WP  WP
 [WP] Adding support for reporting with option: wpreport.
 [WP] Adding support for external proof libraries. See options wpinclude, wptactic, wpcoqlib and wpwhylib.
 [WP] Adding support for multiprovers in command line.
 [WP] Fixing some
bugs.
Release WP 0.4[Nitrogen 20111001]
WP  Ergo
 [Ergo] AltErgo is always used with builtin arrays. Removed option wparrays.
 [Ergo] AltErgo 0.93 now required.
WP  Gui
New Features
 [Gui] Removed 'Refresh' button from WP panel.
 [Gui] Enhancement of ProofObligation panel.
 [Gui] Default output directory is set to <home>/.framacwp in Gui.
 [Gui] New menu options to prove preconditions at one or all call sites.
 [Gui] Feedback for proof of preconditions at call sites.
Bug Fixes
 [Gui] Fixed bug
#711 (cyclic
dependencies).
 [Gui] Fixed bug on PO status (wrong PO identification).
WP  Hoare
 [Hoare] New Hoare model (now implemented on top of logic variables).
WP  Store
 [Store] Better representation of pointers (issue #796).
WP  Vampire
 [Vampire] Support for Vampire as backend prover
WP  WP
New Features
 [WP] No more logic generic pointers. Pointer arithmetics moved to memory models.
 [WP] Better representation of records and unions in logic.
 [WP] AltErgo is now selected (and run) by default.
 [WP] New engine to compute proof obligations for arbitrary invariants. See option wpinvariants
 [WP] Handling partial initializers in C global variables.
 [WP] Translation of axioms with labels (removed option wpaxioms).
 [WP] Added option wpprooftrace to obtain more informations from provers when available (option 'Trace' in GUI).
 [WP] Print of formula change
 [WP] Optimization of arguments passing by reference
 [WP] Improvements of conversion between Cintegers and Zintegers
 [WP] Optimization of arguments passing by reference with option: wpbyreference
 [WP] A warning is now emitted for missing assigns clauses
 [WP] Further improvement for proof of assigns clauses
Bug Fixes
 [WP] Fixed problems with wpout <dir>.
 [WP] In some cases, a proof attempt could silently failed. It is now properly reported.
Release WP 0.3[Carbon 20110201]
WP  Cmd
 [Cmd] Adding version in wphelp.
 [Cmd] Option wpwarnings to display additional informations for 'Stronger' and 'Degenerated' goals.
 [Cmd] Options wpstatusxxx to refine goal selection
 [Cmd] Clarification of save/then effect on WP
WP  Coq
 [Coq] Fixed bug #740 for Coq on Windows. WP now uses directly coqtop compile instead of coqc.
 [Coq] Fixed bug #702 on Coq output with large integers.
WP  Gui
 [Gui] Fixed incorrect property status refresh in the GUI.
WP  Runtime
 [Runtime] Optimization of effectassigns.
WP  Store
 [Store] Fixed bug #766 about offsets in assigns.
WP  WP
 [WP] New spliting algorithm. See option wpsplit. Option wpsplitdim <n> to limit spliting up to 2**n subgoals.
 [WP] When rteprecond is not used, wp generates a separate proof obligation for each call site.
 [WP] Proof of
requires of the main entry point (bug #675).
Release WP 0.2[Carbon 20101202]
WP  Coq
 [Coq] Fixed bug #639: no more compilation to shared directory.
WP  Gui
 [Gui] Accessibility
of all provers from gui.
Release WP 0.1[Carbon 20101201]
WP  WP
 [WP] New WP
plugin.