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

  • Subject: [Frama-c-discuss] Use frama-c with Jessie to analyze multiple files
  • From: x_cui at hotmail.com (Xiao-lei Cui)
  • Date: Thu, 22 Aug 2013 22:35:24 -0400
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>