--- layout: fc_discuss_archives title: Message 76 from Frama-C-discuss on February 2012 ---
On 02/16/2012 11:27 AM, Boris Hollas wrote: > On Wed, 2012-02-15 at 14:55 +0100, Julien Signoles wrote: >>>> Jessie is happy now in simple cases, but I provide no guarantee that it >>>> is enough in all situations... > > I have a strange problem: If I use > > method vfunc _ = begin > let new_kf = Cil.get_kernel_function (Cil.copy_visit ()) (Extlib.the > self#current_kf) in > Kernel_function.set_spec new_kf (fun s -> s); > Cil.SkipChildren > end > in my jessie-prepared copy visitor and call Jessie with Project.on, some > VCs of previously verified code can't be proved. If I don't override > vfunc, Jessie proves all VCs. Shouldn't method vfunc above just copy the > funspec? Using (Cil.copy_visit ()) instead of your own visitor behavior (something like your_visitor#behavior) is a bit strange. Not sure yet your issue comes from here. -- Julien