--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on August 2013 ---
Hi All, I am new to frama-c (Carbon) and jessie(why2.29). I would like to use frama-C to verify a small OS kernel, but I am stuck in passing multiple C files to the tool-chain. I probably did not set the flags correctly. The command I used: frama-c -jessie max.c hello.c Frama-c returns error message: [kernel] preprocessing with "gcc -C -E -I. -dD max.c" [kernel] preprocessing with "gcc -C -E -I. -dD hello.c" [kernel] failure: getReturnType: not a function type [kernel] user error: skipping file "hello.c" that has errors. [kernel] Frama-C aborted because of invalid user input. The two simple files I passed to the tool are max.c and hello.c, global variable gFlags is referenced across files, as listed below /* max.c */ #define ZERO 0 int gFlag =0; /*@ requires x>ZERO; @ ensures \result >= x && \result >= y && \result>ZERO; @ ensures \result == x || \result == y; @*/ int max (int x, int y) { if (x>y) return x; return y; } //-------------------------------------------------------------------------- /*hello.c*/ /*@ @ ensures \result == 0; @*/ extern int gFlag; int foo(void){ return gFlag; } THanks a lot. Tony Cui -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130822/577249a7/attachment-0001.html>