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] Jessie plugin - more than 6, 000 VCs generated

Thank you for all the replies.

Our initial idea was not modify the legacy code, but we implemented the
David's suggestion of creating functions. It has worked very well, reducing
drastically the numbers of VCs and all of them were proved successfully.

We tried the Fran?ois suggestion too, salving the session and it was very
useful.

Best regards,
Nanci

On Fri, Oct 18, 2013 at 4:26 AM, David MENTRE <dmentre at linux-france.org>
 wrote:

>
> You would obtain the same result by putting part of your code into
> another function, with a proper contract to represent the
> corresponding code and call it from the original function. Which
> brings me to a fourth proposal:
>
>  4. Cut the original code into several sub functions, with for each
> called function a contract summarizing the corresponding code.


On Fri, Oct 18, 2013 at 5:28 AM, Fran?ois Bobot <francois.bobot at cea.fr>wrote:
>
> If you are using the plugin Jessie or the plugin WP, you can already prove
> your goal using why3. And why3 has a session mechanism through the commands
> why3ide, why3replayer and why3session. A session allow you the kind of
> cache David is referring.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131031/beca6380/attachment.html>