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

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