--- layout: fc_discuss_archives title: Message 73 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using results of one plugin in another plugin



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