--- layout: fc_discuss_archives title: Message 89 from Frama-C-discuss on February 2012 ---
[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