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