--- layout: fc_discuss_archives title: Message 79 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 12:31 PM, Boris Hollas wrote:
> On Thu, 2012-02-16 at 12:00 +0100, Julien Signoles wrote:
>> 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.
>
> makes no difference.
>
> No I save the project to a file "prj". However, loading it fails with
> Jessie:
>
> $ frama-c -load prj -jessie -jessie-atp="gui"
> [kernel] warning: no input file.
> [jessie] Starting Jessie translation
> [jessie] user error: Nothing to process. There was probably an error
> before.
> [kernel] Plug-in jessie aborted because of invalid user input.
>
> but frama-c-gui -load prj works.

Jessie is not project-compliant. One consequence is unexpected behaviors 
in multi-projects mode (as said before). Another one is unexpected 
behaviors with save/load. A third one is unexected behaviors with -then-on.

As Jessie is not any longer under active development, these features 
might be never supported by this plug-in, except with special fundings.

> Also, how is -then-on used? If I use "-then-on prj" I get "[kernel] user
> error: no project "prj"."

Here 'prj' is not a Frama-C project name but the name of a saved file. 
The project name is chosen by the plug-in which generates it and it is 
its responsibility to document it. Anyway it is possible to infer any 
project name from the 'Project' menu of the Frama-C GUI (not the Jessie 
GUI).

--
Julien