--- layout: fc_discuss_archives title: Message 102 from Frama-C-discuss on October 2013 ---
[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>