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] I wrote a blog post about my experiences with Frama-C so far

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>