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