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?

  • Subject: [Frama-c-discuss] Can i keep WP-proofs while working on other code/annotations?
  • From: ds.verification at flecsim.com (ds.verification at flecsim.com)
  • Date: Fri, 6 Jun 2014 11:40:52 +0200 (CEST)
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