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

[Frama-c-discuss] Kernel functions



Hello Boris,

2012/2/17 Boris Hollas <hollas at informatik.htw-dresden.de>:
>
> 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
>

This code sets a spec related to the new_kf in the current (i.e. old)
project. That's why nothing seems to change: the new_kf does not
correspond to a function in this project (admittedly, the kernel
should complain loudly in such a case). You have to apply set_spec in
the new project, either by putting it in the queue
(self#get_filling_action), or by using Project.on. Using the queue is
the preferred way: all operations on the tables of the new project are
done at the same time, eliminating the cost of multiple context
switch, and the set_spec will be done after new_kf itself has been
registered in the new project (since this event is queued by
Visitor.generic_frama_c_visitor), which will become important if the
kernel starts verifying that you do set_spec on a registered kf.
As an aside, you can use Visitor.frama_c_copy for inheriting from a
generic copy visitor.

> 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.
>

You shouldn't use an inplace visitor as argument of
create_project_visitor (in fact, I thought that the kernel enforced
that, and if it doesn't yet, expect that Oxygen will). All kind of
trouble can happen when there are sharings between two projects.

> 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.

This code is safe. The argument given to a method of a copy visitor is
a new node. On the other hand, its children are still belonging to the
old AST, since the copy is done by the visitor itself.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile