--- layout: fc_discuss_archives title: Message 4 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



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.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile