WP - Gui

• [Gui]  Changes into Gui panel.

WP - WP

• [WP]  Adding support for reporting with option: -wp-report.
• [WP]  Adding support for external proof libraries. See options -wp-include, -wp-tactic, -wp-coq-lib and -wp-why-lib.
• [WP]  Adding support for multi-provers in command line.
• [WP]  Fixing some bugs.
  
  

WP - Ergo

• [Ergo]  Alt-Ergo is always used with builtin arrays. Removed option -wp-arrays.
• [Ergo]  Alt-Ergo 0.93 now required.

WP - Gui

New Features

• [Gui]  Removed 'Refresh' button from WP panel.
• [Gui]  Enhancement of Proof-Obligation panel.
• [Gui]  Default output directory is set to <home>/.frama-c-wp 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 back-end 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]  Alt-Ergo is now selected (and run) by default.
• [WP]  New engine to compute proof obligations for arbitrary invariants. See option -wp-invariants
• [WP]  Handling partial initializers in C global variables.
• [WP]  Translation of axioms with labels (removed option -wp-axioms).
• [WP]  Added option -wp-proof-trace 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 C-integers and Z-integers
• [WP]  Optimization of arguments passing by reference with option: -wp-byreference
• [WP]  A warning is now emitted for missing assigns clauses
• [WP]  Further improvement for proof of assigns clauses

Bug Fixes

• [WP]  Fixed problems with -wp-out <dir>.
• [WP]  In some cases, a proof attempt could silently failed. It is now properly reported.

WP - Cmd

• [Cmd]  Adding version in -wp-help.
• [Cmd]  Option -wp-warnings to display additional informations for 'Stronger' and 'Degenerated' goals.
• [Cmd]  Options -wp-status-xxx 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 effect-assigns.

WP - Store

• [Store]  Fixed bug #766 about offsets in assigns.

WP - WP

• [WP]  New spliting algorithm. See option -wp-split. Option -wp-split-dim <n> to limit spliting up to 2**n sub-goals.
• [WP]  When -rte-precond is not used, wp generates a separate proof obligation for each call site.
• [WP]  Proof of requires of the main entry point (bug #675).
  
  

WP - Coq

• [Coq]  Fixed bug #639: no more compilation to shared directory.

WP - Gui

• [Gui]  Accessibility of all provers from gui.
  
  

WP - WP

• [WP]  New WP plugin.