--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on March 2011 ---
Hello list, On 02-08, Virgile Prevosto wrote: > > 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. Virgile's point is nicely illustrated by trying an alternative of specifying the concrete logic type mentioned before in this thread that *is* accepted at the Frama-C level but rejected by the plug-in wp and jessie: $ cat test2.c /*@ //from frama-c-Carbon-20110201/tests/spec/concrete_type.c type list<A> = Nil | Cons(A,list<A>); axiomatic length { logic integer length<A> (list<A> l); axiom length_empty: length(Nil) == 0; axiom length_cons<A>: \forall A a, list<A> l; length(Cons(a,l)) == length(l)+1; } */ void test() { /*@ assert length(Nil) == 0; */ /*@ assert length(Cons(1,Nil)) == 1; */ } $ frama-c -jessie -jessie-atp alt-ergo test2.c .. [kernel] preprocessing with "gcc -C -E -I. -dD test2.c" [jessie] Starting Jessie translation [kernel] State_builder.aborted because of unimplemented feature. Please send a feature request at http://bts.frama-c.com with: 'Interp.annotation Dtype'. Similar with the wp plug-in (with frama-c-Carbon-20101202-beta2). $ frama-c -wp -wp-proof alt-ergo test2.c .. test2.c:9:[wp] warning: Warning for Axiom length_cons: From wp: logic type variables not yet implemented Effect: Ignored user-defined axiom 'length_cons' .. To understand directions (a third person has asked me about this, the context was to playfully explore some more concise specification for lists than e.g. https://VCC.svn.codeplex.com/svn/vcc/Test/testsuite/examples/List.c ), do either wp and/or jessie plan to go for datatypes? Best, -- Holger Blasum