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

No subject



kf in the new project. 

> 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

So new_kf doesn't corresponds to the kf in the new project?
What's the difference between 
  Extlib.the self#current_kf
and
  Cil.get_kernel_function (self#behavior) (Extlib.the self#current_kf)
if both refer to the current project?

> 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

do I have to register new_kf explicitly or is this done by the copy
visitor?

> You shouldn't use an inplace visitor as argument of
> create_project_visitor (in fact, I thought that the kernel enforced

what should be used to create an inplace visitor? Is it easier to use an
inplace visitor if I change specs, but don't rearrange the AST?

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

In this case, I visit a funspec, which shouldn't have children. However,
the documentation of set_spec says: "You must call this function to
modify a spec and you must not modify directly the 'spec' field of the
record yourself." On the other hand, the line
  s.spec_behavior <- (Cil.empty_funspec ()).spec_behavior;
is much clearer to me than the kf/new_kf related code.

-- 
Best regards,
Boris