Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

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