Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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