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]

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