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]

[no subject]

1. decompose the proof of the assertion by applying tactics into the TIP (Frama-C/Gui, WP proof panel)
Sometimes, by a simple split or range tactic, you can decompose a very complex proof into smaller, simpler ones.

2. make intermediate assertions, and/or write ACSL lemmas. Once you are convinced into your lemmas, you can silent their proofs by turning them into axioms, or add `-wp-prop=- at lemmas` on your command line.

3. use ghost functions to implement the so-called techniques of lemma-functions to decompose the proof into smaller ones.

Hope this help…
	L.

> Le 15 avr. 2019 à 11:36, Tomas Härdin <tjoppen at acc.umu.se> a écrit :
> 
> 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
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss