--- layout: fc_discuss_archives title: Message 85 from Frama-C-discuss on February 2012 ---
Hello Boris, 2012/2/17 Boris Hollas <hollas at informatik.htw-dresden.de>: > > 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 > 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 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 the preferred way: all operations on the tables of the new project are done at the same time, eliminating the cost of multiple context switch, and the set_spec will be done after new_kf itself has been registered in the new project (since this event is queued by Visitor.generic_frama_c_visitor), which will become important if the kernel starts verifying that you do set_spec on a registered kf. As an aside, you can use Visitor.frama_c_copy for inheriting from a generic copy visitor. > 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. > You shouldn't use an inplace visitor as argument of create_project_visitor (in fact, I thought that the kernel enforced that, and if it doesn't yet, expect that Oxygen will). All kind of trouble can happen when there are sharings between two projects. > 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. 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. Best regards, -- E tutto per oggi, a la prossima volta Virgile