--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on February 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Is it possible to define polymorphic axioms? memcpy etc



mån 2020-02-03 klockan 21:02 +0100 skrev Virgile Prevosto:
> Hello again,
> 
> Le 01/02/2020 à 16:14, Tomas Härdin a écrit :
> > Yeah this is what I had in mind. Use make and sed to generate headers
> > containing copies of memcpy() for all desired data types (including
> > structs), then #define say memcpy_uint8_t memcpy when not doing
> > verification
> > 
> 
> a colleague of mine just reminded me that a new plugin of Frama-C has been 
> merged recently and is thus now available on 
> https://git.frama-c.com/pub/frama-c to solve exactly this problem. See 
> https://git.frama-c.com/pub/frama-c/blob/master/src/plugins/builtin/README.md 
> for more information.

Ooh, that looks like just what I need :) So we can expect that this
will land in Scandium sometime this year?

/Tomas