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

Hello,

2012/2/17 Boris Hollas <hollas at informatik.htw-dresden.de>:
>
> From that, I concluded that new_kf in my code above corresponds to the
> 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?

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
project, so that it must be used in the
context of the new project when you apply it to new_kf. Otherwise,
you'll mix information between the two projects, which is always a bad
idea.

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

This is done by the copy visitor (via the queue, this is why it is
better to use the queue also for set_spec: the registration of new_kf
is then guaranteed to occur before).

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

It's always easier to use an inplace visitor, but the real question
is, does it play well with the rest of Frama-C. In particular, a
visitor removing annotations (who might have been used by some
analysis to check a property) should not be inplace (unless you're
operating in your own project, obtained by a previous copy).

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

Of course a funspec has children: they are all the fields of the
record. In this context, children is to be understood as everything
below the current node of the AST.

> 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

this is related to the spec field of the kf record, which is treated
specially. This is handled internally by the generic visitor and
should be transparent for the user

> ?s.spec_behavior <- (Cil.empty_funspec ()).spec_behavior;
> is much clearer to me than the kf/new_kf related code.

Well, if you only operate at the funspec level, it is indeed better to
overload the vspec method. Overloading the vfunc method makes sense if
you generate a spec based for instance on the function body.

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