--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on November 2018 ---
Hello Tomas, Le mer. 21 nov. 2018 à 12:02, Tomas Härdin <tjoppen at acc.umu.se> a écrit : > > As I've written earlier on this list, I'm still a beginner. But I think > someone might still find my experiences so far useful, so I decided to > document them: > > http://www.härdin.se/blog/2018/11/20/trying-out-frama-c/ > <http://www.xn--hrdin-gra.se/blog/2018/11/20/trying-out-frama-c/> > > Thanks for sharing your experience. It is always interesting for us to have feedback on how Frama-C gets used in order to understand where improvements would be the most useful(*) In particular, your point about separation of strings warrant some thinking about \separated hypotheses that can be safely made by the memory models of WP. Regarding termination of recursive functions, this is indeed not yet implemented by WP, but ACSL introduces a decreases clause, which is similar to a loop variant: any recursive call must be done on a strictly smaller 'decreases' term than its direct caller, and that term must stay positive. Currently, WP will emit a warning message if it encounters a decreases clause, saying that this is unsupported. However, for single recursive functions, a simple syntactic transformation should be able to generate an ACSL assertion at each recursive call from the content of the decreases clause. For mutual recursion, things are slightly more tricky (you have to identify all functions involved in the recursion), but this should be doable. Finally, the point about verification time is just a matter of perspective: just wait until Frama-C get a proper C++ front-end, and I'm sure we will be able to have a smaller execution time than the (C++) compiler ð. On a more serious note, as was highlighted by one of our partners, the comparison should rather be done with the time taken by running a test suite with an extremely high level of coverage, a task which is not exactly free. Of course, this does not preclude us from trying to achieve better performances, but formal verification is unlikely to become costless at some point. Thanks again for your post, and feel free to ask further questions on Frama-C. Best regards, -- E tutto per oggi, a la prossima volta Virgile (*) Note however that this email does not in any way indicate whether support for \separated hypothesis or for decreases clause will appear in Frama-C 19 Potassium or not ð -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181121/42189baf/attachment.html>