--- layout: fc_discuss_archives title: Message 36 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



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