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] 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