[Frama-c-discuss] I wrote a blog post about my experiences with Frama-C so far

Virgile Prevosto virgile.prevosto at m4x.org
Wed Nov 21 16:07:31 CET 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>


More information about the Frama-c-discuss mailing list