--- layout: fc_discuss_archives title: Message 67 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



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>