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）」を選択し、メイン関数で「WPによる関数注釈の証明」を実行します。(または、「WP の目標」タブに移動し、そこから Why3 IDE を実行します。) Why3 が表示されたら、選択した証明者を呼び出してすべてを緑色に変更し、セッションを保存して Why3 を終了しますが、Frama では何も起こりません。 -C GUI: プロパティはまだオレンジ/「確認しようとしましたが、決定できませんでした」とマークされています。

Why3 によって生成された証明を実際に使用するように Frama-C に指示するにはどうすればよいですか? 証明自体は間違いなくそこにあります。Why3 をもう一度開いても、すべてが緑色のままなので、セッションは適切に保存されています。また、Frama-C は何かが起こったことを認識しています。Why3 IDE が開いている間、小さな歯車の記号が WP の目標タブに表示され、Why3 を閉じると消えます。

(この特定の特性は、Why3 を使用しなくても Alt-Ergo で証明できることはわかっていますが、より難しい問題には Why3 が必要です。)

4

2 に答える 2

2

私自身への暫定的な回答: Why3 セッション XML ファイルに対する Frama-C のパーサーは、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 に答える