Формат слабых предварительных условий, напечатанных wp-плагином

Question

Я не понимаю формат wp, напечатанный wp-плагином в frama-c. Пример:

Goal Assertion 'P402926' (file gzip-1.5/deflate.c, line 479): 
Let x_0 = Mint_0[(shift match_8 1)]. 
Let x_1 = Mint_0[(shift scan_16 1)]. 
Let x_2 = Mint_0[(shift scan_17 1)]. 
Let a_0 = (global G_window_2513). 
Let x_3 = Mint_0[(shift a_0 (1+cur_match_1))]. 
Let x_4 = Mint_0[scan_17]. 
Let x_5 = Mint_0[(shift a_0 cur_match_1)]. 
Assume { 
    (* Domain *) 
    Type: (is_sint32 best_len_1) /\ (is_sint32 len_0) 
     /\ (is_uint32 cur_match_1) /\ (is_uint8 Mint_0[match_0]) 
     /\ (is_uint8 Mint_0[match_1]) /\ (is_uint8 Mint_0[match_2]) 
     /\ (is_uint8 Mint_0[match_3]) /\ (is_uint8 Mint_0[match_4]) 
     /\ (is_uint8 Mint_0[match_5]) /\ (is_uint8 Mint_0[match_6]) 
     /\ (is_uint8 Mint_0[scan_1]) /\ (is_uint8 Mint_0[scan_3]) 
     /\ (is_uint8 Mint_0[scan_5]) /\ (is_uint8 Mint_0[scan_7]) 
     /\ (is_uint8 Mint_0[scan_9]) /\ (is_uint8 Mint_0[scan_11]) 
     /\ (is_uint8 Mint_0[scan_13]) /\ (is_uint8 x_4) /\ (is_uint8 x_0) 
     /\ (is_uint8 x_1) /\ (is_uint8 x_2) /\ (is_uint8 x_5) 
     /\ (is_uint16 
(* gzip-1.5/deflate.c:453: Else *) 
    Have: x_4=x_5. 
    (* gzip-1.5/deflate.c:454: Else *) 
    Have: x_2=x_3. 
    (* gzip-1.5/deflate.c:468: Conditional *) 
    If: x_0=x_1 
    Then { 
    (* gzip-1.5/deflate.c:468: Conditional *) 
    If: Mint_0[(shift match_8 2)]=Mint_0[(shift scan_16 2)] 
    Then { 
     (* gzip-1.5/deflate.c:469: Conditional *) 
     If: Mint_0[(shift match_8 3)]=Mint_0[(shift scan_16 3)] 
     Then { ..... 

Многие дополнительные переменные были введены, которые я не понимаю, как сдвиг, глобальный, и т.д., которые не находятся в программе ..

Может кто-нибудь объяснить?

Answer 1

Вы можете найти краткое описание внутреннего языка, используемого WP для создания доказательных обязательств в главах 3 и 4 из the WP manual. Кроме того, встроенные функции и предикаты, которые фигурируют в формуле, определены в различных файлах в $(frama-c -print-share-path)/wp/why3, особенно Memory.why, которые аксиоматизируют все операции, связанные с памятью.

Чтобы ответить на ваши основные допросов:

1. if-else здесь, чтобы избежать экспоненциального раздутия числа обязательств доказательства в отношении к количеству ветвей каждой функции (за счет чуть более сложная формула)
2. global берет адрес глобальной сети. Здесь вы можете видеть, что a0 затем используется в качестве индекса на карте Mint_0 (который сопоставляет адреса базы форм + смещение со значениями).
3. shift перемещает смещение адреса: shift a_0 cur_match_1 относится к соответствующей ячейке массива window.