--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on April 2019 ---
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