--- layout: fc_discuss_archives title: Message 6 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?



> Now, I want to get the information of annotation //@ ensures \result
> == ((i<j)?j:i); , including the structure, the s emantic etc.
> Just like we use AST, CFG to represent a C program.
> I wonder whether you konw what I want.

The data structures can be found in [cil/src/cil_types.mli].
For instance, to find your "ensures" property, you first have
to find the [kernel_function] using functions from [Globals.Functions]
(find_by_name or iter for instance). Then, [Kernel_function.get_spec]
returns a [Cil_types.spec] which has a [spec_behavior] field.
In the [b_post_cond] field, you'll find the ensures property.

For internal properties (inside function), you have to use functions
from [Annotations]. Don't use the [Code_annot] from the AST.

Does this answer your questions ?

Bye,
-- 
Anne.