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