--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] usage of Frama_C_memcpy



> You can still verify functions that call memset with this specification.

Sorry, I was carried away by my own argumentation. In the case
of memset and in the current state of Frama-C, you cannot
easily verify functions that call memset either because there are
again pointer casts at the call site.
But you can give ACSL specifications to these functions, and
hopefully, verify with Jessie the functions that call these. My
point was that ACSL tries to be technique-agnostic and not
to embed limitations that come with one tool or another,
and that the verification done by Jessie is compositional,
so when limitations are encountered, these remain contained
to some part of the code base.

Pascal