--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on January 2020 ---
Hi 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? In other words, something like this: /*@ type T; @ requires valid_dest: valid_or_empty(dest, n); @ requires valid_src: valid_read_or_empty(src, n); @ requires separation: @ \separated(dest+(0..(n/sizeof(T))-1),src+(0..(n/sizeof(T))-1)); @ assigns dest[0..(n/sizeof(T)) - 1] \from src[0..(n/sizeof(T))-1]; @ assigns \result \from dest; @ ensures copied_contents: memcmp{Post,Pre}<T>((T*)dest,(T*)src,n/sizeof(T)) == 0; @ ensures result_ptr: \result == dest; @*/ extern void *memcpy(void *restrict dest, const void *restrict src, size_t n); 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. /Tomas