--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on December 2009 ---
> 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