wp插件打印的最弱前置条件格式

Question

我不明白frama-c中wp插件打印的wp格式。一个例子：

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 { .....

引入了很多我不理解的额外变量，比如 shift、global 等，它们不在程序中..

谁能解释一下？

Answer 1

您可以在 the WP manual 的第 3 章和第 4 章中找到 WP 用于构建证明义务的内部语言的简要说明。此外，公式中出现的内置函数和谓词在$(frama-c -print-share-path)/wp/why3中的各种.why文件中定义，特别是Memory.why，它公理化了所有与内存相关的操作。

回答您的主要问题：

if-else在这里是为了避免证明义务的数量相对于每个函数的分支数量呈指数级增长（以稍微复杂的公式为代价）
global 获取全局地址。您可以在此处看到 a0 然后用作 Mint_0 映射中的索引（它将 base + offset 形式的地址映射到值）。
shift移动一个地址的偏移量：shift a_0 cur_match_1指的是window数组对应的单元格。

wp插件打印的最弱前置条件格式

Format of weakest precondition printed by wp plugin

frama-c