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

  • Subject: [Frama-c-discuss] Kernel functions
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Fri, 17 Feb 2012 08:36:54 +0100
  • In-reply-to: <CA+yPOVgEsa8OAjeF2YF1HD4Q1qRYhDwpzi7BhE2AyDAWgh18=Q@mail.gmail.com>
  • References: <1329204516.12949.148.camel@iti27.informatik.htw-dresden.de> <CA+yPOVgEsa8OAjeF2YF1HD4Q1qRYhDwpzi7BhE2AyDAWgh18=Q@mail.gmail.com>
On Tue, 2012-02-14 at 11:39 +0100, Virgile Prevosto wrote:
> 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).

I still have problems with visitors and kernel functions. From what
Virgile wrote, I'd expect this code

inherit Visitor.generic_frama_c_visitor prj (Cil.copy_visit ())
method vspec s = begin
  let new_kf = Cil.get_kernel_function (self#behavior) (Extlib.the
self#current_kf) in
  Kernel_function.set_spec new_kf (fun _ -> Cil.empty_funspec ());
  Cil.DoChildren
end

to clear all funspecs in the AST of the new project. However, both the
AST of the current and of the new project are unchanged.

If I use an inplace_visit instead, all funspecs are cleared. However,
loop annotations are removed in the project returned by
File.create_project_from_visitor, but not in the current project. I
don't understand this as current and new project should be identical in
an inplace visitor.

In contrast, the code

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.
-- 
Best regards,
Boris