--- layout: fc_discuss_archives title: Message 58 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 11:41 +0100, Julien Signoles wrote:
> in multi-projects mode. You can try to call the following function 
> before computing the AST of the initial project (and thus at least 
> before calling File.create_project_from_visitor).
> 
> let prepare_jessie () =
>    Kernel.SimplifyCfg.on ();
>    Kernel.KeepSwitch.on ();
>    Kernel.Constfold.on ();
>    Kernel.PreprocessAnnot.on ();
>    Cabs2cil.setDoTransformWhile ();
>    Cabs2cil.setDoAlternateConditional ()
> 
> Jessie is happy now in simple cases, but I provide no guarantee that it 
> is enough in all situations...

I tried it on a complicated source file and it works.

Jens Gerlach suggested in private mail to use option -then. I tried
-then -jessie -jessie-atp=gui after calling my plugin, but it didn't
work as I expected. My plugin is supposed to erase all function
contracts by

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 fs -> Logic_utils.clear_funspec
fs; fs);
    Cil.SkipChildren
end

but they are still present in Jessie. If I set the current project to
File.create_project_from_visitor, then the input for Jessie is empty.

-- 
Best regards,
Boris