--- layout: fc_discuss_archives title: Message 82 from Frama-C-discuss on February 2012 ---
On Tue, 2012-02-14 at 11:39 +0100, Virgile Prevosto wrote: > 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). I still have problems with visitors and kernel functions. From what Virgile wrote, I'd expect this code inherit Visitor.generic_frama_c_visitor prj (Cil.copy_visit ()) method vspec s = begin let new_kf = Cil.get_kernel_function (self#behavior) (Extlib.the self#current_kf) in Kernel_function.set_spec new_kf (fun _ -> Cil.empty_funspec ()); Cil.DoChildren end to clear all funspecs in the AST of the new project. However, both the AST of the current and of the new project are unchanged. If I use an inplace_visit instead, all funspecs are cleared. However, loop annotations are removed in the project returned by File.create_project_from_visitor, but not in the current project. I don't understand this as current and new project should be identical in an inplace visitor. In contrast, the code inherit Visitor.generic_frama_c_visitor prj (Cil.copy_visit ()) method vspec s = begin s.spec_behavior <- (Cil.empty_funspec ()).spec_behavior; Cil.DoChildren end clears all behaviors in the new project and leaves the current one unchanged. However, I'm unsure as to which fields of the AST are filled at the time of the visit and whether this code is safe. -- Best regards, Boris