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: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Sat, 1 Feb 2020 15:29:47 +0100
  • In-reply-to: <a0fe61903cc8e7929a590f71c27e71532cfd1dab.camel@acc.umu.se>
  • References: <a0fe61903cc8e7929a590f71c27e71532cfd1dab.camel@acc.umu.se>
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