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] ACSL type casting and function pointer issue

Hi all,
   Unfortunately, The code(part of OS kernel) I am trying to work on, consists of plenty of 
function pointers and type conversion from pointers to integer. Jessie 
stops processing whenever it encounters  such features. 
   Is there some way to let jessie by-pass the unsupported type casting and function pointers, and generate VCs for supported features? I wonder.  
   On a second thought, what other options, may be another plug-in or tool, do I have to work around such problems? Any advise?
   Thanks a lot.

cheers,
xiaolei
From: x_cui at hotmail.com
To: frama-c-discuss at lists.gforge.inria.fr
Date: Tue, 26 Nov 2013 20:37:44 -0500
Subject: [Frama-c-discuss] ACSL type casting and function pointer issue




Hi,
   There may be plenty of discussions on type cast and function pointers already, and I am probably looking for the same answers to work around:)
   The code I am trying to verify contains many function pointers and nasty explicit type casting, like the two scenario shown below. Any advise would be appreciated. 
   Thanks.  
xiao-lei 

----------------------------------------------------
1) type casting error on the predicate definition goes as the following:

jessie complains
 [jessie] failure: Casting from type ? to type struct unsigned_intP * not allowed in logic

the code and ACSL annotation:

#define UARTAR                ( ((volatile UINT * )0x01f800e0) )                
#define UARTBR                ( ((volatile UINT * )0x01f800e4) )        

extern volatile UINT * UART_status_register;
extern volatile UINT * UART_data_register;

/*@
predicate  SerialBaudPostCond = (UART_data_register == UARTAR) || (UART_data_register == UARTBR);
*/

------------------------------------------------------
2) for annotation contains function pointers, jessie raised a error message and exited.
":0:[jessie] failure: Function pointer type void () not allowed"

the code segment goes like :

typedef void   (*VOIDFUNCPTR) ();
/*@ ensures (vec_number > 0xFF) || (\null == routine) ==> \result==ERROR;
int itp_connect(UINT vec_number, VOIDFUNCPTR routine, INT parameter)
{
}
 		 	   		  

_______________________________________________
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/20131127/2e3dbe6e/attachment-0001.html>