--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on April 2010 ---
On Tue, 20 Apr 2010, Claude Marche wrote: > 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* ? which why gives me /usr/bin/why so I guess I now finally made a complete mess of this instalation ;) >> 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); > thanks - that helps a lot - I can write up examples, but the goal is to work on existing code - and that was kind of a show-stoper - admitedly I'm not into the manual(s) far enough yet thx! hofrat