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