--- layout: fc_discuss_archives title: Message 95 from Frama-C-discuss on February 2012 ---
[Sorry for the previous message, I should have been more careful with Gmail's shortcuts] 2012/2/21 Boris Hollas <hollas at informatik.htw-dresden.de>: > > I add preconditions based on the formals, so I better work with vfunc. > Well, you can use Kernel_function.get_formals in vspec for that, but there is indeed the issue of discriminating between a function's contract and a statement's contract (self#current_stmt will be None in the former case and Some stmt in the latter). That said, it should also be fine to do it in vfunc. In fact, it's possible to tell vglob not to visit the spec by using a ChangeTo in vglob_aux: method vglob_aux g = match g with | GFun(f,l) -> let new_f = Visitor.visitFramacFunction self f in ChangeTo (GFun(new_f,l)) | _ -> DoChildren > Anyway, really good documentation is needed to understand all this. But > why not convert set_spec to a method, so set_spec can extract the right > kf by itself and properly handle the action, based on self#behavior? > Because set_spec is a generic function that can be used in many other contexts. Basically, what you suggest is what is done by vglob in Visitor.frama_c_generic_visitor, when the spec has been visited by vspec. >> > For an inplace visitor, what should be used instead of >> > File.create_project_from_visitor? >> > >>> >>> Visitor.visitFramacFile or Visitor.visitFramacFileSameGlobals >> > This brings up another problem: how do I get the Cil_types.file? It > doesn't work with Cil.dummyFile. Ast.get Best regards, -- E tutto per oggi, a la prossima volta Virgile