--- layout: fc_discuss_archives title: Message 12 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?



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
>