--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on August 2013 ---
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 listFrama-c-discuss at lists.gforge.inria.frhttp://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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130823/b898e1a0/attachment.html>