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

[Frama-c-discuss] concrete logic types



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