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

2012/2/20 Boris Hollas <hollas at informatik.htw-dresden.de>:
> 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
>

Ahem, that's right, the visitor tries to be smarter than it really is.
The (old) specification
is visited at the global level, and this is the copy of that that you see.
Adding
method vspec _ = Cil.ChangeTo (Cil.empty_funspec ())

will do what you want. As Julien said, vspec is probably the good
place to start anyway if you're operating on the spec alone.

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

new_kf is a copy of kf, which will represent the function in the new
project (since we're in the middle of building this new project, all
tables are not filled yet in this new project. new_kf must be used to
set kernel functions related information, but not to retrieve them).
self#current_kf refers to the AST of the current project (the one that
is currently visited). This project is already built, and information
can be retrieved from it the usual way. On the other
hand, its tables must not be changed by the copy visitor.

> 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 get_* functions are used for nodes that are shared across the AST
(such as varinfo for instance). So it's not "a" copy of the old value,
it's THE only copy that should be used in the new AST. Breaking
sharing would cause random issues in the new project. This is also the
reason why set_* should be used with care.

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

In the default visitor, it happens at the first occurrence of the node
in the AST (for varinfo, it would be its declaration).


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

Visitor.visitFramacFile or Visitor.visitFramacFileSameGlobals

> 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

The queueing is done to postpone operations on the new project at the
end of the visit, so as to have only one context switch (a costly
operation) per visit. It's useless for the inplace visitor since
there's only project involved.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile