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] Warnings for call to memcpy()... why?


Le jeu. 18 juil. 2019 à 17:27, Roderick Chapman <rod at> a
écrit :

> Hello again,
>  Another possibly dumb question: in my code, I have a few calls to
> memcpy() to achieve the effect of whole-array assignment - essentially
> copying the entire content of one array onto another.
> For each of those calls, I am getting a 2 warnings from WP (version 19)
> like this:
>   Cast with incompatible pointers types (source: uint8*) (target: sint8*)
> I get one of those for both the "src" and "dest" parameters of memcpy().
> I don't understand this for several reasons.
> 1. My actual parameters are both type "uint8_t *"
> 2. The formal parameters given in the declaration of memcpy() in
> libc/string.h are
> "void *restrict dest", and "const void *restrict src".
> So.. where are these references to "uint8*" and "sint8*" coming from?
> There are no such types in my program.
> How do I get rid of these warnings?

Generally speaking, WP is quite bad at handling memcpy and other functions
of its ilk  (memset, memmove, memcmp, ...), as having to deal with void
pointers breaks its memory model, which is strongly based on the type with
which each object is declared (a new memory model based on more general
memory regions is rumored to appear at some point in the future, though).
In theory, `-wp-model +cast` is able to do a little bit more in this
direction, but I'm not very optimistic about it. A code transformation on
the model of the variadic plug-in which would produce specialized versions
of memcpy (and its specification) for each type with which it is used would
probably be more suitable, but it does not exist as far as I know.

Regarding your question about uint8* and sint8*, these are the counterpart
in the logic model built by WP of uint8_t* and void* respectively (for some
reason, WP chooses to somehow equate void* with char*)

Best regards,
E tutto per oggi, a la prossima volta
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <>