[SOLVED] How to use Why3 proofs in Frama-C GUI?

How to use Why3 proofs in Frama-C GUI?

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.)

Solution

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.