frama-c - Frama-C 無効化 wp qed

Question

オプション -wp-out を指定して Frama-C WP を使用する場合、たとえば (swap.c の例を使用): 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 ;
}  

実行する:

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

そして出力付き：

[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)

プロパティを証明し、プログラムの妥当性を証明するために必要な証明義務を含むフォルダーを生成しますが、すべてではなく、Alt-ergo に送信されたものだけが Qed によって証明されるものは生成されません。

Qed の目的は単純化し、自明な特性を証明して証明者の時間と労力を節約することだと理解していますが、証明者に送信するすべての証明義務を生成させることは可能ですか? これは、Qed を無効にして Frama-C にすべての証明義務をオルターゴに生成させることですか?