--- layout: fc_discuss_archives title: Message 64 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)? It is difficult to response precisely to your question since there is not a full compilable and reproducible case. However, an uncaught exception is always a bug in the tool. So please report a bug on the BTS (http://bts.frama-c.com). -- Julien