--- layout: fc_discuss_archives title: Message 82 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Kernel functions



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