--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on July 2011 ---
> 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.