--- layout: fc_discuss_archives title: Message 40 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 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
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130822/577249a7/attachment-0001.html>