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

Boris wrote:

>Hello Stephane,
>
>what is the builtin Frama_C_memcpy function? Is it related to the libc memcpy function?

Frama_C_mempcy is a builtin function that is recognized by the value analysis.
Until the time when the value analysis can interpret such ACSL specifications
as can be written for library functions like memcpy, we are making do
with algorithmic descriptions that sometimes use special built-in
functions.

Boris: your disappointment not being able to prove an actual implementation
of memset satisfies its specification is natural, and the value analysis'
built-ins are *not* a solution to this problem, only workarounds for
different problems that happen to be located in the same functions.
But there is a silver lining:
you *can* write memset's specification in ACSL. It's only the verification of
an implementation wrt this specification that currently isn't supported in Jessie.
You can still verify functions that call memset with this specification.
Since the limitation is not in ACSL itself, someday you can expect
to be able to be able to prove memset itself, and until then,
the fact that one can convince him/herself that memset actually implements
the specification in a human code review is the kind of thing that can
be accepted by a certification authority.

St?phane: Frama_C_memcpy's implementation as a built-in function is
partial. That's why it is not documented :) 
(I know, it shouldn't be in .../share/frama_c/libc.c then. Please consider
that this is the real bug).
I used it for experiments when I handled dynamic memory allocation by
unrolling so much that Frama_C_memcpy was never called (in the
analysis) on ambiguous arguments that could represent several addresses.

It is possible to complete the implementation of this built-in to
handle ambiguous arguments, the only reason it was not done is that
is was not needed at the time. A workaround it to define memcpy
by a C implementation instead of trying to use this built-in.

Pascal