--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on June 2014 ---
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