郵資-C禁用WP QED

Question

當使用郵資-C WP與-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爲alt-ergo生成所有證明義務？

Answer 1

有兩個主要選項來管理Qed將在每項證明義務上的工作量。的-wp-help輸出提供了以下提示：

• -wp-no-simpl防止簡單化常數項和謂詞
• -wp-no-let防止展開局部變量的

如果同時使用，你應該能夠獲得最證明您的po_out目錄中的義務，或多或少是由WP計算得出的（請注意，某些PO可能仍會排出Qed，例如，如果您有//@ assert \true;某處）。