--- layout: fc_discuss_archives title: Message 76 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 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