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

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