--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on February 2020 ---
Hello, Le 01/02/2020 à 16:14, Tomas Härdin a écrit : >> contracts) quantified over types. What you'd like to have amounts to a >> restricted form of C++ templates (i.e. >> memcpy<T>(T* x, T* y, size_t len) { ... }), and the current solution used by >> frama-clang is to only handle full instantiations (relying on clang to do >> said instantations) and treat them independently from each other. > > Interesting. Does that mean frama-c is able to reason "yes both > pointers involved are of the same time so everything looks fine to me" > when using clang? How do I enable this? > Sorry, my mail was confusing. Frama-Clang is the (pretty experimental) C++ front-end of Frama-C, and the template instantiation I referred to is done by clang as a normal phase of type-checking a C++ program. There's no possibility to do that with C code. > > 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 > Well my idea was to use the Frama-C programmatic API (hence OCaml), since you can have directly access to the type of the actual arguments of memcpy, which is more complicated to do with sed, but I guess that if you're ready to replace the calls by hand, generating the corresponding prototypes can indeed be automated that way. Best regards, -- E tutto per oggi, a la prossima volta Virgile