--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on April 2013 ---
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? Best Regards, Beno?t GERARD [ENVOYE PAR INTERNET] -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130426/63106102/attachment.html>