--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on August 2013 ---
Hi, The use of -pp-annot option could be usefull in order to pre-process your annotations. > frama-c -kernel-help -pp-annot pre-process annotations (if they are read) (opposite option is -no-pp-annot) Kind regards, Patrick. Le 23/08/2013 04:35, Xiao-lei Cui a ?crit : > > 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 > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? nettoy?e... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130823/7d228bd9/attachment.html>