--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on June 2014 ---
Hello Lo?c, thank you for commenting, unfortunately the C source in question is too large to fit into Why3, so i take it from the docs (wp-manual-Neon-20140301.pdf pg. 16) that CVC4 cannot be used. Still i'm curious how to handle a large code base. Usually i need quite a few runs before having the annotations of a function straightened so WP can discharge it's contract as a whole. So i guess i will just have to spend the time for these runs until the function is "finished"? Best regards, Daniel Lo?c Correnson schrieb am 06.06.2014 14:33: > 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 >