--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on June 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Can i keep WP-proofs while working on other code/annotations?



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>