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

  • Subject: [Frama-c-discuss] pointer to interrupt
  • From: jean-marc.harang at c-s.fr (Jean-Marc Harang)
  • Date: Tue, 02 Nov 2010 18:04:07 +0100
  • In-reply-to: <AANLkTikoeBjrxxKz__CFkfbaMN32Wo-NZwfesPQVWWUn@mail.gmail.com>
  • References: <4CC933FD.4050604@c-s.fr> <AANLkTikoeBjrxxKz__CFkfbaMN32Wo-NZwfesPQVWWUn@mail.gmail.com>
Le 28/10/2010 10:36, Pascal Cuoq a ?crit :
> 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.
>
>    

Thanks ! It's working. I used the same method for some special other 
keywords if the keyword is unknown.

best regards,
-- 
jean-marc Harang