Type declaration using reals in ACSL/Frama-C -

Type declaration using reals in ACSL/Frama-C -

i have issues acsl specification lastly frama-c version. tried lot of things declare pair of reals, none of them worked. here tiny illustration illustrating problem :

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

which gives :

[kernel] user error: unexpected token '('

at end, want have code near :

/*@ axiomatic realpairs { type real_pair = (real, real); logic real norm ( real_pair p ) = \let (x,y) = p; \sqrt(x*x + y*y); } */

does see error ? found acsl documentation vague on type declarations...

thank much answers.

best regards,

nilexys.

what have written right respect acsl manual. however, can see in acsl implementation manual (http://frama-c.com/download/frama-c-acsl-implementation.pdf), pairs not supported in current implementation of acsl in frama-c. in fact, thing partially supported in area of acsl sum types. more precisely, can define sum types, \match construction not supported frama-c, means have resort axiomatics. in current state of affairs, next should accepted 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; */

c frama-c