--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Specification modules - Sets and Maps



Hi everyone,

I hope I'm not doing a repeated question but I tried to find information about the use of specification modules (section 2.6.11 in the ACSL manual) and I did not succeed. 

I just would like to know if this feature is working or not, because I would like to use a specification module of sets and maps(section 3.1.3) and I don't know how to do it.

Moreover, I guess that these kind of type declarations

type list<A> = Nil | Cons(A,list<A>);

are not supported yet, right? I tried to used them but the compilation with frama-c together with the jessie plug-in raises the following error:

[jessie] failure: Unexpected exception.
                  Please submit bug report (Ref. "Extlib.NotYetImplemented("Interp.annotation Dtype")")

Thanks.
Best regards,
B?rbara Vieira
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101015/010f9fb5/attachment.htm>