--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on April 2010 ---
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 make: *** [hello.stat] Error 127 [jessie] user error: Jessie subprocess failed: make -f hello.makefile gui so the problem obviously was primarily the "trivial" example - nice example of perception limitations... thanks ! > > I put a reading list on > http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=en:frama-c > May I suggest you try the examples from one of the documentation > dependency chain in order? will do that. > > (I will update this page soon to refer to new versions of Frama-C, > Why/Jessie, and ACSL by Example) > many thanks ! hofrat