--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on October 2009 ---
Thank you for helping. Now it works well. Best regards, Chen 2009/10/15 Claude Marche <Claude.Marche at inria.fr> > Hi, > > I confirm that the problem is due to missing .whyrc, which is generated > by running > > why-config > > In earlier versions, there was a more friendly message, I will investigate. > > - Claude > > Virgile Prevosto wrote: > > Hello, > > > > Le jeu. 15 oct. 2009 14:18:38 CEST, > > geng chen <chengeng4001 at gmail.com> a ?crit : > > > > > >> tang at tang-desktop:~/Desktop$ frama-c-gui -jessie ./first.c > >> > > > > In fact, you don't need to call frama-c-gui: the jessie plug-ins uses > > Why's graphical interface, which is a different thing. > > > > > >> Generating Why function main > >> gwhy-bin [...] why/first.why > >> Computation of VCs... > >> Computation of VCs done. > >> Reading GWhy configuration... > >> Config file '/home/tang/.gwhyrc' does not exists, using default config > >> Fatal error: exception Not_found > >> make: *** [first.stat] Error 2 > >> > >> > > > > Did you run why-config (the script that detects which provers are > > installed on your system) after the installation? gwhy is supposed to > > ask you to do so when it's not the case, but it might have failed to > > do so for some reason. > > > > Regards, > > > > > -- > Claude March? | tel: +33 1 72 92 59 69 > INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 > Parc Orsay Universit? | fax: +33 1 74 85 42 29 > 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ > F-91893 <http://www.lri.fr/%7Emarche/%0AF-91893> ORSAY Cedex > | > > > > > > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091015/468b0f59/attachment.htm