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] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing swap.c (with preprocessing)
[kernel] Parsing swap2.h (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Collecting axiomatic usage
[rte] annotating function swap
[wp] 9 goals scheduled
[wp] [Alt-Ergo] Goal typed_swap_post_A : Valid
[wp] [Qed] Goal typed_swap_post_B : Valid
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_swap_assert_rte_mem_access_2 : Valid
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_3 : Valid
[wp] [Qed] Goal typed_swap_assert_rte_mem_access_4 : Valid
[wp] [Qed] Goal typed_swap_assign_part1 : Valid
[wp] [Qed] Goal typed_swap_assign_part2 : Valid
[wp] [Qed] Goal typed_swap_assign_part3 : Valid
[wp] Proved goals:    9 / 9
     Qed:             6
     Alt-Ergo:        3
----------------------------------------------------------
Functions           WP   Alt-Ergo    Total   Success
swap                 6      3 (17)     9       100%
----------------------------------------------------------

Requirements

Recommanded provers (to be installed separately):

User Manual and Tutorial

For more details about the WP plug-in, including installation instructions, please consult the WP manual and use the Frama-C mailing lists
WP Plug-in Manual

The Fraunhofer Fokus Team provides an extensive corpus of ACSL annotations for typical C programs to be proved by WP. It is available online and a public repository hosts the annotated source examples:

Other previous tutorials on deductive verification of C programs with Frama-C plug-ins Jessie or WP can be helpful as well:

Publications: