--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on January 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



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