--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on June 2014 ---
Hi, Can you please send us your proof obligations generated for Alt-Ergo in order to test them on the current devel version ? Regards, Mohamed. Le 6 juin 2014 14:33, "Lo?c Correnson" <loic.correnson at cea.fr> a ?crit : > 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 > > _______________________________________________ > 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 > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140606/4420ac63/attachment.html>