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

Question

这感觉像是一个愚蠢的问题，但我很困惑。我正在尝试使用 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, select "Why3 (ide)" 作为证明者，运行 "Prove function annotations by WP" 作为主函数。（或者：我导航到 "WP goals" 选项卡，然后从那里导航到运行 Why3 IDE。）Why3 出现，我调用我选择的证明者将所有内容变为绿色，保存会话并退出为什么 3，然后在 Frama-C GUI 中没有任何反应：属性仍然标记为橙色/"tried to verify but could not decide"。

如何让 Frama-C 实际使用 Why3 生成的证明？ 证明本身肯定在那里：如果我再次打开 Why3，一切仍然是绿色的，所以会话已正确保存。此外，Frama-C 意识到某事已经发生：当 Why3 IDE 打开时，WP 目标选项卡中可以看到一个小齿轮符号，当我打开时它会消失关闭 Why3.

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

Answer 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 开发人员，谁能发表评论？

Answer 2

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

但是，我们希望与 Why-3 会话更紧密地集成，并将证明者履行每项证明义务的情况导入回 Frama-C。事实上，我们将在本次重构期间修复该错误。

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

How to use Why3 proofs in Frama-C GUI?

frama-c

why3