--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on August 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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 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>