--- layout: fc_discuss_archives title: Message 119 from Frama-C-discuss on November 2013 ---
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>