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] 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