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



lör 2020-02-01 klockan 15:29 +0100 skrev Virgile Prevosto:
> Hello,
> 
> Le 31/01/2020 à 19:06, Tomas Härdin a écrit :
> 
> > So in Frama-C 20.0 memcpy() is defined with void* and the associated
> > axioms use char* when necessary. Would it be possible to instead have
> > these axioms so that if src and dest are both the same type, and n is a
> > multiple of sizeof(*src) then it behaves as if the types of the input
> > were of this same type?
> > 
> > 
> > AFAICT it's not possible to do things like \exists type T; [...]
> > 
> > There's not a lot of documentation how to use polymorphic stuff in
> > Frama-C hence this e-mail.
> > 
> 
> You're right, it is not possible to have formulas (not to speak about whole 
> 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?

> Moreover, in the current Frama-C implementation (although pure ACSL permits 
> it), you cannot speak about a pointer to T with T a type variable, hence no
> 
> predicate memcmp<T>(T* p1, T* p2, integer len) =
>    \forall integer i; 0 <= i < len ==> p1[i] == p2[i];
> 
> even though it would be of little use to write contracts over C functions 
> taking void* parameters.
> 
> A workaround would be to have a plug-in that performs the instances 
> beforehand (i.e. memcpy_char, memcpy_int, memcpy_double, ...), with the 
> caveat that if there are some kinds of wrappers around memcpy in the code 
> base, some sort of transitive closure might be needed.

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

/Tomas