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