Frama-C disabling wp qed

Question

When using Frama-C WP with the option -wp-out, for example(using swap.c example): swap.c

// 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 ;
}  

Executing with:

$frama-c -wp -wp-out po_out swap.c

And with output:

[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[jessie3] Looking up module mach.int.Int32
[jessie3] Looking up module mach.int.Int64
[kernel] preprocessing with "clang -C -E -I.  swap.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 5 goals scheduled
[wp] [Qed] Goal typed_swap_post_B : Valid
[wp] [Qed] Goal typed_swap_assign_part1 : Valid
[wp] [Alt-Ergo] Goal typed_swap_assign_part2 : Valid (39ms) (21)
[wp] [Alt-Ergo] Goal typed_swap_post_A : Valid (Qed:1ms) (38ms) (13)
[wp] [Alt-Ergo] Goal typed_swap_assign_part3 : Valid (30ms) (21)
[wp] Proved goals:    5 / 5
     Qed:             2  (0ms-1ms)
     Alt-Ergo:        3  (30ms-39ms) (21)

It proves the properties and generates a folder with the proof obligations required to prove the proprieties of the program, but not all, only the ones sent to Alt-ergo the ones that Qed proves are not generated.

I understand the purpose of the Qed is to simplify, prove trivial properties to save the prover time and effort, but is it possible to let it generate all the proof obligations to send to the prover? This is, disabling Qed and let Frama-C generate all proof obligations to alt-ergo?

Answer 1

There are two main options that govern the quantity of work that Qed will do on each proof obligation. The output of -wp-help gives the following hints:

• -wp-no-simpl prevents simplification constant terms and predicates
• -wp-no-let prevents unfolding of local variables

If you use both, you should be able to obtain most proof obligations in your po_out directory, more or less as they have been computed by WP (note that some PO might still be discharged by Qed, e.g. if you have //@ assert \true; somewhere).