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