--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] why-2.24 install question



Le mar. 20 avril 2010 12:19:21 CEST,
Nicholas Mc Guire <der.herr at hofr.at> a ?crit :

> On Tue, 20 Apr 2010, Pascal Cuoq wrote:
> 
> > > the hello.c is really just a trivial example for testing
> > > #include <stdio.h>
> > >
> > > void foo(void)
> > > {
> > > ? ? ? ?printf("hello,world\n");
> > 
> > The notion of "trivial" is relative. Your example includes standard
> > headers that contain horrible stuff, and calls a variadic function.
> > Jessie behaved as well as you can expect on your example: your
> > installation is fine.
> 
> not quite - removed the printf and the include and provided a dummy function
> get
> 
> rtl26:~/formal_methods/Frama-C/examples# frama-c.byte -jessie hello.c
> [kernel] preprocessing with "gcc -C -E -I.  -dD hello.c"
> [jessie] Starting Jessie translation
> [jessie] Producing Jessie files in subdir hello.jessie
> [jessie] File hello.jessie/hello.jc written.
> [jessie] File hello.jessie/hello.cloc written.
> [jessie] Calling Jessie tool in subdir hello.jessie
> Generating Why function foo
> Generating Why function main
> [jessie] Calling VCs generator.
> gwhy-bin [...] why/hello.why
> /bin/sh: gwhy-bin: command not found

This suggests that the graphical user interface is missing. Do you have
the lablgtk library installed? If not, neither why nor frama-c will
complain (you can see a warning about lablgtk in config.log though), but
they will only build the command-line tools. If you have some provers
installed (e.g. alt-ergo), you can directly select one of them with
-jessie-atp <prover> (e.g. -jessie-atp alt-ergo).

Hope this helps,
-- 
E tutto per oggi, a la prossima volta.
Virgile