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

[Sorry for the previous message, I should have been more careful with
Gmail's shortcuts]

2012/2/21 Boris Hollas <hollas at informatik.htw-dresden.de>:
>
> I add preconditions based on the formals, so I better work with vfunc.
>

Well, you can use Kernel_function.get_formals in vspec for that, but
there is indeed the issue of discriminating between a function's
contract and a statement's contract (self#current_stmt will be None in
the former case and Some stmt in the latter). That said, it should
also be fine to do it in vfunc. In fact, it's possible to tell vglob
not to visit the spec by using a ChangeTo in vglob_aux:
method vglob_aux g = match g with
 | GFun(f,l) -> let new_f = Visitor.visitFramacFunction self f in
ChangeTo (GFun(new_f,l))
 | _ -> DoChildren

> Anyway, really good documentation is needed to understand all this. But
> why not convert set_spec to a method, so set_spec can extract the right
> kf by itself and properly handle the action, based on self#behavior?
>

Because set_spec is a generic function that can be used in many other
contexts. Basically, what you suggest is what is done by vglob in
Visitor.frama_c_generic_visitor, when the spec has been visited by
vspec.

>> > For an inplace visitor, what should be used instead of
>> > File.create_project_from_visitor?
>> >
>>>
>>> Visitor.visitFramacFile or Visitor.visitFramacFileSameGlobals
>>
> This brings up another problem: how do I get the Cil_types.file? It
> doesn't work with Cil.dummyFile.

Ast.get

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