--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on May 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Logical annotations



On May 7, 2009, at 10:23 AM, PAREAUD, Thomas wrote:
>
>
> Each time I tried to write "\sum" annotations, I obtain errors such as
> "ignoring logic specification of function XXX" or other errors.
>
> Do you have any idea about the reasons of such errors?

ACSL is a language that is being defined separately from
the implementation of the tools that use it. The constructs
you are using are part of ACSL but not yet supported in Jessie.

I believe that I pointed you to the messages
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000453.html
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000457.html
in the past. They are still as relevant today as they were then.

Pascal

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090507/c5ada860/attachment.htm