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