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

[Frama-c-discuss] Annotation pre-processing



Hello,

2013/4/26  <benoit.gerard at dga.defense.gouv.fr>:
> First thanks to the community for the fast answering (and the new version).
>
> I may have missed something concerning pre-processing of annotations and the
> option -pp-annot but I would like to be able to write something of the form
>
> #define SIZE 32
> //@ requires \valid(tab+(0..SIZE-1));
> void f( int *tab );
>
> When launching Frama-C it induces an error (unbounded variable SIZE in
> annotation).
> I assume this is linked to the fact that SIZE is a parameter of the
> predicate.
> Is this a bug or a known limitation of the -pp-annot option?
>

This is a known limitation of C preprocessor. 0..SIZE is in fact a
preprocessing number according to section 6.4.8 of C99 standard[1],
i.e. a single pre-processing token. SIZE is thus not seen as a macro
identifier. To overcome that, you can simply put a space between ..
and SIZE (and/or 0).

Best regards,
--
E tutto per oggi, a la prossima volta
Virgile
[1] The rationale behind this still escapes me.