Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Is it possible to "save"/reuse proofs?
  • From: tjoppen at acc.umu.se (Tomas Härdin)
  • Date: Mon, 15 Apr 2019 11:36:03 +0200
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