--- layout: fc_discuss_archives title: Message 119 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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)
{
}
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131126/9e651b6d/attachment.html>