--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on April 2010 ---
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