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