--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on October 2011 ---
Hello St?phane, On 28/10/2011 17:04, DUPRAT Stephane wrote: > Hello, > > I'm working on a new Frama-C project built by the cmd > "File.create_project_from_visitor" and I lose the ACSL contract if a > make a change to a global function. > > For example, if have a copy visitor like this: > > inherit Visitor.frama_c_copy prj method vglob_aux g = match g with | > GFun (_) -> Cil.ChangeTo [g] > > All functions have lost their contract in the copy project. Is there > a way to keep contracts of the original function ? Perhaps throw the > kernel_functions, but they are not handle by the visitor. > As a rule of thumb, whenever you use SkipChildren or ChangeTo in a visitor, the visit stop there. In particular, since a function contract is considered somehow as a child of the global it belongs to, the contract will not be visited, (and not copied in the new project when you have a copy visitor). By the way, the use of ChangeTo in your code snippet is incorrect: the function (and in particular its statements, the varinfos of formals and globals, etc.) are shared between original and new projects. In fact, ChangeTo g should only be used in a copy visitor if g has been built from scratch by the visitor (that must also add to the action queue the registration of the new contract if needed). Developer's manual suggests to use ChangeDoChildrenPost(g,fun x -> x) instead, to ensure that all the nodes will be visited and copied. Best regards, -- E tutto per oggi, a la prossima volta Virgile