How to use Why3 proofs in Frama-C GUI?

Question

This feels like a silly question, but I'm stumped. I'm trying to use Frama-C Sodium and Why3 0.86.1 (both installed via OPAM) to prove some simple properties. Consider this program (toy.c):

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

I want to prove this assertion using the Frama-C GUI and Why3. So I run frama-c-gui toy.c, select "Why3 (ide)" as the prover and run "Prove function annotations by WP" on the main function. (Alternatively: I navigate to the "WP goals" tab and run the Why3 IDE from there.) Why3 appears, I call the prover of my choice to turn everything green, save the session and quit Why3, and then nothing happens in the Frama-C GUI: The property is still marked orange/"tried to verify but could not decide".

How do I tell Frama-C to actually use the proofs produced by Why3? The proofs themselves are definitely there: If I open Why3 again, everything is still green, so the session was saved properly. Also, Frama-C is aware that something has happened: While the Why3 IDE is open, a little cogwheel symbol is visible in the WP goals tab, and it disappears when I close Why3.

(I realize that this particular property can be proved by Alt-Ergo without involving Why3, but I do need Why3 for harder problems.)

score 2 · Answer 1 · answered Sep 17 '15 at 19:55

Preliminary answer to myself: It looks like Frama-C's parser for the Why3 session XML file doesn't match the XML generated by Why3 0.86.1. This patch seems to fix this:

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

No guarantees that this will work for anyone else (or even that it's correct for my own uses, although I do think so).

Any Frama-C developers here, by any chance, who could comment?

score 1 · Accepted Answer · answered Sep 18 '15 at 09:45

Thanks for reporting the bug. The proposed fix seems to work.

However, we would like to integrate more tightly with Why-3 sessions, and import back to Frama-C which prover(s) discharged each proof obligation. Indeed, we will fix the bug during this refactoring.

How to use Why3 proofs in Frama-C GUI?

2 Answers2