--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on February 2020 ---
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