--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on August 2013 ---
Works well now, thanks for the tip. cheers, tony Date: Fri, 23 Aug 2013 10:29:51 -0300 From: richard.bonichon at gmail.com To: frama-c-discuss at lists.gforge.inria.fr Subject: Re: [Frama-c-discuss] Use frama-c with Jessie to analyze multiple files Hey, It is because you put your ACSL annotation above the "extern int gFlag" part, which is indeed not a function. The annotation should just before the function as follows extern int gFlag; /*@ @ ensures \result == 0; @*/ int foo(){ return gFlag; } On Fri, Aug 23, 2013 at 3:22 AM, Xiao-lei Cui <x_cui at hotmail.com> wrote: Hi , Thanks for the tip. I should set the -pp-annot flag. But the problem seems to remain the same way, cuix at berkhoff:~/projects/frama-c$ frama-c -pp-annot max.c hello.c [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] error occurring when exiting Frama-C: stopping exit procedure. Frama-C aborted because of invalid user input. Removing the cross referenced global variable, the files are analyzed properly. but is this intended? Any suggestions? tony Date: Fri, 23 Aug 2013 07:27:25 +0200 From: Patrick.Baudin at cea.fr To: frama-c-discuss at lists.gforge.inria.fr Subject: Re: [Frama-c-discuss] Use frama-c with Jessie to analyze multiple files 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 _______________________________________________ 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 _______________________________________________ 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 -- Richard Bonichon _______________________________________________ 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130824/19c54206/attachment-0001.html>