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

2012/2/14 Boris Hollas <hollas at informatik.htw-dresden.de>
> - why doesn't
>
> method vfunc f = begin
> Foo.feedback "%a\n" Cil.d_funspec f.sspec;
> Cil.SkipChildren
> end
>
> give the same result as
>
> method vfunc _ = begin
> let kf = Extlib.the self#current_kf in
> let fs = Kernel_function.get_spec kf in
> Foo.feedback "%a\n" Cil.d_funspec fs;
> Cil.SkipChildren
> end
>
> ??? (the former doesn't print anything, the latter shows the contract)

Because annotations are stored in the AST only in the early phase of
AST construction (namely until link). Once all tables have been
filled, field sspec is empty, and there are neither Code_annot node
nor code_annotation in Loop nodes. As mentioned in section 5.15, one
must use accessor functions provided by Frama-C's kernel to retrieve
this information.

>
> - why does this not work in example 5.14.7:
>
> ????? let kf = Extlib.the self#current_kf in
> ????? Queue.add (fun () -> Annotations.add_assert kf stmt [Ast.self] assertion) self#get_filling_actions;
>
> ??? (instead, using Cil.get_kernel_function works)

Because you have a copy visitor. self#current_kf refers to the
kernel_function in the current project, while you want to add an
annotation in the new project, that has another kernel_function
(Projects do not share anything, their purpose is to keep analyses
separated). Cil.get_kernel_function (and its twin
Cil.get_original_kernel_function) allows to retrieve the corresponding
kf in the new project (and vice-versa).

> - why are the fields of type kernel_function mutable (and also the fields of many other records)?

It's more convenient (but admittedly trickier) to use mutable fields
in some places. For instance, you can have a GVarDecl and a GFun for
the same function, that will thus share the same kf. This kf can be
created when processing the GVarDecl (for processing the function's
contract), and then updated when encountering the GFun. Without
mutable fields, this would be slightly more complicated.

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