--- layout: fc_discuss_archives title: Message 89 from Frama-C-discuss on February 2012 ---
On Fri, 2012-02-17 at 17:26 +0100, Virgile Prevosto wrote: > 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 Now I've queued set_spec but it doesn't work either: inherit Visitor.frama_c_copy prj method vfunc _ = begin let new_kf = Cil.get_kernel_function (self#behavior) (Extlib.the self#current_kf) in let action () = Kernel_function.set_spec new_kf (fun _ -> Cil.empty_funspec ()) in Queue.add action self#get_filling_actions; Cil.DoChildren end > 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 Ok, but what really is new_kf as opposed to kf? I still don't see how this statement > Cil.get_kernel_function allows to retrieve the corresponding > kf in the new project and >> the new_kf does not correspond to a function in this project agree. What do kf and new_kf mean and refer to when the copy visitor visits a node? In 5.14.5, what does "get_name gets the copy corresponding to an old value" mean, is it a copy of the old value, is it the value of a node k in the copied AST such that old value is stored at node k in the original AST? The next bullet says: "set_name sets a copy for a given value. Be sure to use it before any occurrence of the old value has been copied". When exactly does this copy operation happen? > visitor removing annotations (who might have been used by some > analysis to check a property) should not be inplace (unless you're I plan to add annotations. I remove them as an exercise before I proceed with more difficult tasks. For an inplace visitor, what should be used instead of File.create_project_from_visitor? Is it right that actions of a copy visitor must be queued but not those of an inplace visitor (at least it seems to work that way in my inplace visitor)? Why is that so? -- Best regards, Boris