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

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.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile