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] pointer to interrupt

Bonjour,

On Thu, Oct 28, 2010 at 10:27 AM, Jean-Marc Harang
<jean-marc.harang at c-s.fr> wrote:
> I got ?an error "[kernel] user error: syntax error" ?after the preprocess of
> a header file with value analysis with the following declaration :
>
> typedef interrupt void (*SYS_T_PINT) (void);
>
> This declaration is used after for a interrupt vector array... I know it's
> very low level but it's a classic feature for embedded software.

Function pointers are supported by the front-end of Frama-C.
Individual plug-ins may support them or not at their convenience. For
the value analysis, it's easy to support them so so they are. For
Jessie and its design-by-contract philosophy, additional features
would be required in the specification language to express the
contract expected of a function pointer (I think).

> In this case, what is the best way to solve / avoid the problem ??

If the target code only uses the keyword 'interrupt" as in the example
you gave, use:

#define interrupt

This makes the typedef a valid, standard C definition of a function
pointer type SYS_T_PINT.

Regards,

Pascal