--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on January 2012 ---
kf in the new project. > 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 So new_kf doesn't corresponds to the kf in the new project? What's the difference between Extlib.the self#current_kf and Cil.get_kernel_function (self#behavior) (Extlib.the self#current_kf) if both refer to the current project? > 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 do I have to register new_kf explicitly or is this done by the copy visitor? > You shouldn't use an inplace visitor as argument of > create_project_visitor (in fact, I thought that the kernel enforced what should be used to create an inplace visitor? Is it easier to use an inplace visitor if I change specs, but don't rearrange the AST? > > 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. In this case, I visit a funspec, which shouldn't have children. However, the documentation of set_spec says: "You must call this function to modify a spec and you must not modify directly the 'spec' field of the record yourself." On the other hand, the line s.spec_behavior <- (Cil.empty_funspec ()).spec_behavior; is much clearer to me than the kf/new_kf related code. -- Best regards, Boris