Type declaration using reals in ACSL/Frama-C

Question

I have some issues with ACSL specification for the last Frama-C version.
I tried a lot of things to declare a pair of reals, but none of them worked. Here is a tiny example illustrating by problem :

/*@ type real_pair = (real, real); */

Which gives :

[kernel] user error: unexpected token '('

At the end, I want to have a code near to :

/*@ axiomatic RealPairs { 

type real_pair = (real, real);  

logic real Norm ( real_pair p ) =   
\let (x,y) = p;  
\sqrt(x*x + y*y);  

} */

Does someone see where the error is ? I found the ACSL documentation very vague on the type declarations...

Thank you very much for your answers.

Best regards,

Nilexys.

Virgile Virgile · Accepted Answer · 2014-06-23T07:02:26

What you have written is correct with respect to the ACSL manual. However, as you can see in the ACSL Implementation manual (http://frama-c.com/download/frama-c-acsl-implementation.pdf), pairs are not supported in the current implementation of ACSL in Frama-C. In fact, the only thing that is partially supported in this area of ACSL is sum types. More precisely, you can define sum types, but the \match construction is not supported by Frama-C, which means that you have to resort to axiomatics. In the current state of affairs, the following should be accepted by Frama-C (not tested though):

/*@ type real_pair = RPCons(real, real); */
/*@ axiomatic Real_pair {
     logic real rp_fst(real_pair p);
     logic real rp_snd(real_pair p);
     axiom rp_fst_def: \forall real x, y; rp_fst(RPCons(x,y)) == x;
     axiom rp_snd_def: \forall real x,y; rp_snd(RPCons(x,y)) == y;
 */

Type declaration using reals in ACSL/Frama-C

1 Answers