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

On Fri, 2012-02-17 at 17:26 +0100, Virgile Prevosto wrote:
> 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

Now I've queued set_spec but it doesn't work either:

inherit Visitor.frama_c_copy prj
method vfunc _ = begin
  let new_kf = Cil.get_kernel_function (self#behavior) (Extlib.the
self#current_kf) in
  let action () = Kernel_function.set_spec new_kf (fun _ ->
Cil.empty_funspec ()) in
  Queue.add action self#get_filling_actions;
  Cil.DoChildren
end


> Sorry, I might not have been clear. new_kf is to be used in the new
> project indeed. set_spec has an impact on the internal state of the

Ok, but what really is new_kf as opposed to kf? I still don't see how
this statement

> Cil.get_kernel_function allows to retrieve the corresponding
> kf in the new project

and

>> the new_kf does not correspond to a function in this project

agree. What do kf and new_kf mean and refer to when the copy visitor
visits a node?

In 5.14.5, what does "get_name gets the copy corresponding to an old
value" mean, is it a copy of the old value, is it the value of a node k
in the copied AST such that old value is stored at node k in the
original AST?

The next bullet says: "set_name sets a copy for a given value. Be sure
to use it before any occurrence of the old value has been copied". When
exactly does this copy operation happen?

> visitor removing annotations (who might have been used by some
> analysis to check a property) should not be inplace (unless you're

I plan to add annotations. I remove them as an exercise before I proceed
with more difficult tasks.

For an inplace visitor, what should be used instead of
File.create_project_from_visitor?

Is it right that actions of a copy visitor must be queued but not those
of an inplace visitor (at least it seems to work that way in my inplace
visitor)? Why is that so?
-- 
Best regards,
Boris