--- layout: fc_discuss_archives title: Message 22 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



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