--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on February 2011 ---
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.