frama-c - 如何在 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，选择“Why3 (ide)”作为证明者，然后在主函数上运行“Prove function annotations by WP”。 (或者:我导航到“WP 目标”选项卡并从那里运行 Why3 IDE。)Why3 出现，我调用我选择的证明程序将所有内容变为绿色，保存 session 并退出 Why3，然后 Frama 中没有任何反应-C GUI:该属性仍标记为橙色/“已尝试验证但无法决定”。

我如何告诉 Frama-C 实际使用 Why3 生成的证据？证据本身确实存在:如果我再次打开 Why3，一切仍然是绿色的，因此 session 已正确保存.此外，Frama-C 意识到发生了某事:当 Why3 IDE 打开时，WP 目标选项卡中会显示一个小齿轮符号，当我关闭 Why3 时它会消失。

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

Answer 1

我自己的初步答案:看起来 Frama-C 的 Why3 session 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 开发人员，谁可以发表评论？