WP plug-in

The WP plug-in implements a weakest precondition calculus for ACSL annotations through C programs.

For each code annotation, this technique generates a bundle of proof obligations, ie. mathematical first-order logic formula that can be submit to automated theorem provers like Alt-Ergo or interactive proof assistants like Coq. Other provers are also supported via the Why platform.

Tutorial Example

Consider the following short C function:

// File swap.c:

/*@ requires \valid(a) && \valid(b);
  @ ensures A: *a == \old(*b) ;
  @ ensures B: *b == \old(*a) ;
  @ assigns *a,*b ;
  @*/
void swap(int *a,int *b)
{
  int tmp = *a ;
  *a = *b ;
  *b = tmp ;
  return ;
}
To run the WP on this simple example, you may use: 
# frama-c -wp -wp-rte -wp-proof alt-ergo swap.c
[kernel] preprocessing with "gcc -C -E -I.  swap.c"
[kernel] preprocessing with "gcc -C -E -I.  swap2.c"
[rte] annotating function swap
[wp] [WP:simplified] Goal store_swap_function_assigns : Valid
[wp] [Alt-Ergo] Goal store_swap_assert_4_rte : Valid
[wp] [Alt-Ergo] Goal store_swap_assert_3_rte : Valid
[wp] [Alt-Ergo] Goal store_swap_assert_2_rte : Valid
[wp] [Alt-Ergo] Goal store_swap_assert_1_rte : Valid
[wp] [Alt-Ergo] Goal store_swap_post_1_A : Valid
[wp] [Alt-Ergo] Goal store_swap_post_2_B : Valid

Requirements

Supported provers (to be installed separately):

User Manual and Tutorial

For more details about the WP plug-in, including installation instructions, please consult the draft manual and tutorial below, and use the Frama-C mailing lists:
WP Plug-in Manual
WP Plug-in Tutorial and its examples.
The tutorial is based on the excellent "ACSL By Example" book produced by the Fraunhofer FIRST Institute.

The source package of the plug-in is available from the Download Center.