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



Nicholas Mc Guire wrote:
> 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
>   
strange, are you sure you did "make install" ?

What is the result of  ls -l /usr/local/bin/*why* ?
>  so the problem obviously was primarily the "trivial" example - nice example
> of perception limitations... thanks !
>   
Limitations are listed in the manual:

http://frama-c.com/jessie_tutorial_index.html#htoc20

I suggest to start with examples of the tutorial, instead of "hello world"

About varyadic functions: for the moment I do not feel this is essential for
program verification applications. The ACSL specification language does
not say how to give contracts to such functions anyway.

In practice, a typical workaround can be declaring a specific instance e.g

/*@ requires \valid(format);
   @ assigns \nothing;
   @*/
int printf(const char *format);


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