--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on April 2019 ---
mÃ¥n 2019-04-15 klockan 11:56 +0200 skrev Loïc Correnson: > Hi Tomas, > > I think you didnât miss anything at all. > There is not (yet) any cache mechanism in WP to reuse previous proofs > from one session to the other. > Although, we are working to implement such a feature, among many > others ! Sounds promising :) > In the short term, there are several workarounds you can try to > improve the situation. > From my point of view, a proof requiring 30s timeout is far too > complex, so try either to: > > 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. I did this in this case, performing just a single computation in each statement and breaking up the assertions accordingly. This worked well to speed things up > 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. Yes, I've found the turn-lemmas-into-axioms approach useful. Or as I like to call it: the "because I say so"-method > 3. use ghost functions to implement the so-called techniques of > lemma-functions to decompose the proof into smaller ones. I read about ghost functions just the other day. I will have to give them a try some time Thanks for the tips, most useful /Tomas