Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

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