--- layout: fc_discuss_archives title: Message 68 from Frama-C-discuss on April 2013 ---
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.