--- layout: fc_discuss_archives title: Message 41 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



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>