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