--- layout: fc_discuss_archives title: Message 79 from Frama-C-discuss on February 2012 ---
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