Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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
>