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

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>