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

[Frama-c-discuss] how to interpret ACSL annotations?



Hello,

Le 03/07/2011 12:28, ??? a ?crit :
>
> For example, there is a function max as follow which appears in page 3
> ,jessie-tutorial:
>
> //@ ensures \result == ((i<j)?j:i);
> int max(int i, int j)
> {
> return (i<j)?j:i;
> }
>
> Now, I want to get the information of annotation //@ ensures \result ==
> ((i<j)?j:i); , including the structure, the semantic etc.
> Just like we use AST, CFG to represent a C program.
> I wonder whether you konw what I want.

The types of annotations are part of Cil_types among the other types of 
the AST.

These annotations are available in 3 different modules:
- Globals.Annotations for global annotations (e.g. lemmas)
- Annotations for code annotations (e.g. assertions)
- Kernel_function for function contracts

It is also possible to visit annotations by using a Frama-C visitor.

The semantics is given by the ACSL reference manual, in the same way 
that the semantics of the C program is given by ISO C 99.

Hope this helps,
Julien Signoles