--- layout: fc_discuss_archives title: Message 2 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?



Hi

I've been eyeing over the ACSL spec and the frama-c manpage to see if
it's possible to keep/reuse expensive proofs, or generate ACSL code
corresponding to them, in some human-readable format. I currently have
one assertion in a function that computes an average that takes 30
seconds for Z3 to prove, which is a bit annoying.

I gave -save and -load a try, but those mostly seem to exist to be able
to resume a frama-c run. Likewise -session doesn't seem to do much. I
feel like I'm missing something obvious..

My invocation currently looks like this:

  frama-c -wp -wp-rte -wp-timeout 30 -warn-unsigned-overflow -wp-prover 
z3,cvc4,alt-ergo,qed proven.c

What am I missing?

/Tomas