Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Is it possible to define polymorphic axioms? memcpy etc

  • Subject: [Frama-c-discuss] Is it possible to define polymorphic axioms? memcpy etc
  • From: tjoppen at acc.umu.se (Tomas Härdin)
  • Date: Fri, 31 Jan 2020 19:06:21 +0100
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