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