--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on February 2012 ---
Hello Boris, 2012/2/14 Boris Hollas <hollas at informatik.htw-dresden.de> > - why doesn't > > method vfunc f = begin > Foo.feedback "%a\n" Cil.d_funspec f.sspec; > Cil.SkipChildren > end > > give the same result as > > method vfunc _ = begin > let kf = Extlib.the self#current_kf in > let fs = Kernel_function.get_spec kf in > Foo.feedback "%a\n" Cil.d_funspec fs; > Cil.SkipChildren > end > > ??? (the former doesn't print anything, the latter shows the contract) Because annotations are stored in the AST only in the early phase of AST construction (namely until link). Once all tables have been filled, field sspec is empty, and there are neither Code_annot node nor code_annotation in Loop nodes. As mentioned in section 5.15, one must use accessor functions provided by Frama-C's kernel to retrieve this information. > > - why does this not work in example 5.14.7: > > ????? let kf = Extlib.the self#current_kf in > ????? Queue.add (fun () -> Annotations.add_assert kf stmt [Ast.self] assertion) self#get_filling_actions; > > ??? (instead, using Cil.get_kernel_function works) Because you have a copy visitor. self#current_kf refers to the kernel_function in the current project, while you want to add an annotation in the new project, that has another kernel_function (Projects do not share anything, their purpose is to keep analyses separated). Cil.get_kernel_function (and its twin Cil.get_original_kernel_function) allows to retrieve the corresponding kf in the new project (and vice-versa). > - why are the fields of type kernel_function mutable (and also the fields of many other records)? It's more convenient (but admittedly trickier) to use mutable fields in some places. For instance, you can have a GVarDecl and a GFun for the same function, that will thus share the same kf. This kf can be created when processing the GVarDecl (for processing the function's contract), and then updated when encountering the GFun. Without mutable fields, this would be slightly more complicated. Best regards, -- E tutto per oggi, a la prossima volta Virgile