3

这感觉像是一个愚蠢的问题，但我很难过。我正在尝试使用 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 来解决更难的问题。）

4

2 回答 2

2

对我自己的初步回答：看起来 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 开发人员，谁可以发表评论？

于 2015-09-17T19:55:51.343 回答
1

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

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

于 2015-09-18T09:45:32.317 回答