--- layout: fc_discuss_archives title: Message 73 from Frama-C-discuss on February 2012 ---
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? -- Best regards, Boris