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] memcpy / memset question

Hello,

To complement David's answer, here are a few points:

- the function Frama_C_memcpy mentioned in libc.c is actually the name of a
builtin of Value. Builtins are OCaml functions that entirely replace the
corresponding C function of the standard library. They are usually faster
and more precise than what would be obtained by analyzing the body of the C
function itself.

The builtin for memcpy is not available in the open-source version of
Frama-C. It can be found either in the commercial version of Frama-C (
http://frama-c.com/support.html), or in TrustInSoft Analyzer, with minor
variations between the two implementations.

- Without the builtin, a body must be supplied for memcpy. This is the goal
of the various implementations in libc.c.

Still, it seems that this file would benefit from a little dusting. The
proposed implementation of memcpy is not easy to analyze for Value, in
particular when not enough slevel is available to fully unroll the loop.
The implementation below is preferable :

void* memcpy(void* dst, const void* src, size_t n) {

  char* pdst = (char*)dst;
  char* psrc = (char*)src;
  for (size_t i=0; i<n; i++) {
    pdst[i] = psrc[i];
  }
  return dst;
}

- the ifdef FRAMA_C_MEMCPY is in retrospect unhelpful, especially since it
is not set by default. Furthermore, when one uses a version of Frama-C
where the builtin Frama_C_memcpy, is available, there are better solutions
to use it than to provide a body that calls the builtin.

- as mentioned by David, if you need to (mem)copy precise contents, you
will have to crank up the slevel available (up to the maximum value for n).

Hope this helps,


On Tue, Aug 18, 2015 at 10:47 AM, David MENTRE <dmentre at linux-france.org>
wrote:

> Hello Tim,
>
> Le 18/08/2015 07:44, Tim Newsham a écrit :
>
>> test.c:12:[kernel] warning: accessing uninitialized left-value: assert
>> \initialized(&targ[i]);
>>
>> which indicates that the analyzer did not notice that memcpy
>> is initializing all of targ[0..n-1] when doing memcpy(targ, src, n).
>> Is there an easy way to force this in the analysis?
>>
>
> With Value Analysis, you should use both libc.c and builtin.c provided by
> Frama-C standard library to have proper definition of various C standard
> library function as C code (better understood by Value analysis).
>
> But for some reasons, Frama_C_memcpy() defined in builtin.c does not seem
> to work properly. You can use a work around by defining FRAMA_C_MEMCPY
> which uses a C only version.
>
> You also need to increase the -slevel parameter for the loop to 8,
> otherwise Value analysis applies its widening operator and the resulting
> value could be considered uninitialized.
>
>   frama-c -val -cpp-extra-args='-DFRAMA_C_MEMCPY' `frama-c
> -print-share-path`/libc.c `frama-c -print-share-path`/builtin.c -slevel 8
> tim-test.c
>
> Best regards,
> david
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>



-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150826/b8f9209d/attachment-0001.html>