--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on February 2011 ---
Hello, Le lun. 07 f?vr. 2011 13:48:41 CET, Constantin Enea <cenea at liafa.jussieu.fr> a ?crit : > 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? > \match is not supported by Frama-C. In addition to the ACSL manual, which describes the full ACSL language, each version of Frama-C has some implementation notes (in $FRAMAC_SHARE/manuals/acsl-implementation.pdf, also available on http://frama-c.com/download/acsl-implementation-${FRAMAC_VERSION}.pdf) which says in particular which constructions are not currently supported. Note that these implementation notes only cover what is done by the kernel. Plug-ins may themselves add some further restrictions, which, at least theoretically, are described in their respective manuals. Best regards, -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 82 98