--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on April 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Is it possible to "save"/reuse proofs?



mån 2019-04-15 klockan 12:15 +0200 skrev Virgile Prevosto:
> Hello Tomas,
> 
> > Le lun. 15 avr. 2019 à 11:36, Tomas Härdin <tjoppen at acc.umu.se> a écrit :
> 
> > 
> >   frama-c -wp -wp-rte -wp-timeout 30 -warn-unsigned-overflow -wp-prover
> > z3,cvc4,alt-ergo,qed proven.c
> > 
> > What am I missing?
> > 
> 
> As Loïc says, you're not missing anything obvious. However, there exists a
> hack that can allow you to take advantage of Why3's own session mechanism.
> Given the necessary steps, I'm afraid this is not exactly robust, but you
> might nevertheless be interested in the approach. This uses the GUI, but it
> might be possible to write a quick and dirty script that performs the file
> operations in batch mode.
> 
> 1) generate POs without launching provers: frama-c-gui [your options]
> -wp-prover none file.c
> 2) in the WP proofs panel of the GUI, launch Why3 on a PO: this should give
> you a Why3 session with all the PO attached to a given function.
> 3) Use whatever provers and strategies you want in Why3 and save the Why3
> session before quitting Why3 and Frama-C
> 4) copy the why3session.xml in ~/.frama-c-wp/project-session into somewhere
> safe
> 5) redo step 1
> 6) copy why3session.xml into ~/.frama-c-wp/project-session from the place
> where you stored it.
> 7) redo step 2: Why3 should read why3session.xml and reuse the proofs of
> the PO whose statement has not changed since step 3.

I've suspected something like this is possible, especially given -wp-
hints to feed coq scripts to WP. I haven't dived into either coq or
why3 much beyond looking at the output of -wp-out, but I suspect I
eventually will

/Tomas