--- layout: fc_discuss_archives title: Message 42 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 , 
   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 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 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130823/92df8cb5/attachment.html>