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

  • Subject: [Frama-c-discuss] ACSL type casting and function pointer issue
  • From: x_cui at hotmail.com (Xiao-lei Cui)
  • Date: Tue, 26 Nov 2013 20:37:44 -0500
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>