--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on May 2010 ---
I can't test it for the moment, but my guess is that Jessie does not consider BUFF_SIZE as a true constant. I'm not sure if the C norm guarantees that it cannot change. To check if it is the problem, you can try adding BUFF_SIZE == 4 as a precondition. Anyway, the best solution is to keep using #define Expanding the macro definitions in annotations is not a task of Jessie but of Frama-C kernel. See the FAQ or the manual about the --pp-annot option - Claude Boris Hollas wrote: > Jessie is unable to verify the following code for reasons that I don't > understand. I get "?" for postcondition, pointer dereferencing, > arithmetic overflow. Using #define instead of const doesn't work either > because it seems that Jessie doesn't read #defines. > > > const int BUFF_SIZE = 4; > > /*@ requires \valid(msg+(0..BUFF_SIZE)); > ensures msg[BUFF_SIZE] == '\0'; > */ > int setFoo(char* msg) { > msg[BUFF_SIZE] = '\0'; > msg[BUFF_SIZE-1] = '\0'; > return 0; > } > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >