--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on September 2009 ---
hello, one question about syntax in frama-C. why it'not possible to write the following requires; /*@ requires \valid((v.c[0 .. MAXLEN-1])->c[0 .. MAXLEN-1]); */ frama-c -main f e.c -jessie Uncaught exception: File "jc/jc_interp.ml", line 939, characters 25-31: Assertion failed /*@ requires \valid((v.c[0 .. MAXLEN-1])->c+(0 .. MAXLEN-1)); */ frama-c -main f e.c -jessie Uncaught exception: File "jc/jc_interp.ml", line 939, characters 25-31: Assertion failed /*@ requires \valid((v.c+(0 .. MAXLEN-1))->c+(0 .. MAXLEN-1)); */ frama-c -main f e.c -jessie e.c:8:[kernel] user error: Error during annotations analysis: expected a struct with field c something wrong in my predicates or some todos in tools (-> assert false)? many thnx for any help, jc