--- layout: fc_discuss_archives title: Message 10 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,

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