如何在 Frama-C GUI 中使用 Why3 证明？答案

【问题标题】：How to use Why3 proofs in Frama-C GUI?如何在 Frama-C GUI 中使用 Why3 证明？
【发布时间】：2015-09-18 17:45:32
【问题描述】：

这感觉像是一个愚蠢的问题，但我很难过。我正在尝试使用 Frama-C Sodium 和 Why3 0.86.1（均通过 OPAM 安装）来证明一些简单的属性。考虑这个程序（toy.c）：

int main(void) {
    char *hello = "hello world!";
    /*@ assert \valid_read(hello+(0..11)); */
    return 0;
}

我想使用 Frama-C GUI 和 Why3 来证明这个断言。所以我运行frama-c-gui toy.c，选择“Why3 (ide)”作为证明者，然后在主函数上运行“Prove function annotations by WP”。（或者：我导航到“WP 目标”选项卡并从那里运行 Why3 IDE。）出现 Why3，我调用我选择的证明者将所有内容变为绿色，保存会话并退出 Why3，然后在 Frama 中什么也没有发生-C GUI：该属性仍标记为橙色/“尝试验证但无法决定”。

我如何告诉 Frama-C 实际使用Why3 生成的证明？ 证明本身肯定存在：如果我再次打开 Why3，一切仍然是绿色，因此会话已正确保存.此外，Frama-C 知道发生了一些事情：当 Why3 IDE 打开时，WP 目标选项卡中会出现一个小齿轮符号，当我关闭 Why3 时它会消失。

（我意识到 Alt-Ergo 可以在不涉及 Why3 的情况下证明这个特殊属性，但我确实需要 Why3 来解决更难的问题。）

【问题讨论】：

标签： frama-c why3

【解决方案1】：

对我自己的初步回答：看起来 Frama-C 的 Why3 会话 XML 文件解析器与Why3 0.86.1 生成的 XML 不匹配。这个补丁似乎解决了这个问题：

diff -ur frama-c-Sodium-20150201/src/wp/why3_session.ml frama-c-Sodium-20150201-hacked/src/wp/why3_session.ml
--- frama-c-Sodium-20150201/src/wp/why3_session.ml  2015-03-06 16:28:27.000000000 +0100
+++ frama-c-Sodium-20150201-hacked/src/wp/why3_session.ml   2015-09-17 21:35:30.717409735 +0200
@@ -160,6 +160,20 @@
   let name = string_attribute "name" elt in
   name

+let load_result parent_goal r =
+  match r.Xml.name with
+  | "result" ->
+      let status = string_attribute "status" r in
+      assert (parent_goal.goal_verified = false);
+      parent_goal.goal_verified <- (status = "valid")
+  | _ -> ()
+
+let load_proof parent p =
+  match p.Xml.name with
+  | "proof" ->
+      List.iter (load_result parent) p.Xml.elements
+  | _ -> ()
+
 let rec load_goal parent g =
   match g.Xml.name with
   | "goal" ->
@@ -168,7 +182,9 @@
       let mg =
         raw_add_no_task parent gname
       in
-      mg.goal_verified <- verified
+      mg.goal_verified <- verified;
+      (* hack for different(?) session file format *)
+      List.iter (load_proof mg) g.Xml.elements
   | "label" -> ()
   | s ->
       Wp_parameters.debug

不保证这对其他人有效（或者即使我自己认为它是正确的，但我确实这么认为）。

这里有任何 Frama-C 开发人员，谁可以发表评论？

【讨论】：

【解决方案2】：

感谢您报告错误。建议的修复方法似乎有效。

但是，我们希望与 Why-3 会话更紧密地集成，并将其导入回 Frama-C，证明者履行了每个证明义务。事实上，我们会在这次重构中修复这个错误。

【讨论】：