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

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