--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on June 2014 ---
Hi, Keeping previous proofs after reprising is unsafe. However, as you already mention it, the session mechanism of Why-3 can be used for that purpose, since Why-3 is capable of recovering most of previous runs. We are looking forward such a functionality in WP, but it is not available in current release. To improve your situation, you might: - split your specifications into smaller pieces, using logic predicates to encapsulate complex properties without splitting the code itself - use the CVC4 solver, which is experimentally very performant on proof obligations with complex structures like yours Le 6 juin 2014 ? 11:40, ds.verification at flecsim.com a ?crit : > Hello everybody, > > this might be a simple question but i feel a bit lost at the moment. > I have a C function which operates on larger data structures (two > pointers to structs with approx. 30 members each - legacy code, i'm > investigating whether Frama-C can aid in maintaining it). Besides its > intended operation, the function is supposed to maintain some > invariants on these structures. > > The WP plugin of Neon-20140301 is able to discharge the invariants > using alt-ergo, but only with -wp-split turned on and TimeOut, Steps > and Depth limits all turned off. After configuring the Analyses and > hitting Run, it takes over an hour to prove all 25 goals. > > I'm now wondering how such situations are to be dealed with: > When the source code/annotations are modified and "Reparse"-ed in > Frama-C GUI, the WP validations seem getting lost (bubbles turn from > green to yellow again). > > Probably i'm doing something wrong here? When some other function in > the same C file was changed, i would like to keep the proofs done on > the unmodified parts. > > Currently, i would try the following approaches to handle this: > - Split the C module so that each function resides in its own file, so > a change in one function won't affect all the others > - Try and split the troublesome data structures in smaller to limit > the search space of alt-ergo > - I already tried to load the module in question into Why3 via Jessie > but it quit with "Fatal error: out of memory." (generated .mlw > approx. 18000 lines). > > I'm sorry for the long mail, i presume this is a common case but in > wp-manual.pdf i did not find it, so i tried to describe my situation > in detail. > > Any comments are highly appreciated. > > Best regards, > > Daniel > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss