--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on October 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Beryllium does not compile on FreeBSD 7.2



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 ORSAY Cedex                    |