Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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