--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] concrete logic types



Hi all,

I have tried the example for concrete logic types given in Section 2.6.8. of the ACSL 1.5. description and it answers:

why4.c:4:[kernel] user error: syntax error while parsing annotation
[kernel] user error: skipping file "why4.c" that has errors.
[kernel] Frama-C aborted because of an invalid user input.

Line 4 contains the "\match" key word. Do you have any idea why this does not work?

The input file contains:

/*@
@ type list<A> = Nil | Cons(A,list<A>);
@ logic integer list_length<A>(list<A> l) =
@	\match l {
@		case Nil : 0
@ 		case Cons(h,t) : 1+list_length(t)
@	};
@*/

Constantin Enea.