--- layout: fc_discuss_archives title: Message 34 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:
>> will fix the ocaml version and retry - thanks !
> I suggest to try first
>
> frama-c.byte -jessie <some c file>
>
> if it works, I don't think it is crucial to have the native code version.
>

does not seem to work - but I'm really not sure about my installation:

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
[kernel] No code for function printf, default assigns generated
hello.c:5:[jessie] failure: unsupported variadic functions
[jessie] warning: Unsupported feature(s).
                  Jessie plugin can not be used on your code.

the hello.c is really just a trivial example for testing
#include <stdio.h>

void foo(void)
{
        printf("hello,world\n");
}

int main(int argc, char ** argv)
{
        foo();
        return 0;
}


> The crucial part is usually the WP computation, and with the jessie  
> plugin, this is done
> externally by calling the why command, and hopefully this is done in  
> native mode.
>

thx!
hofrat