--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on September 2009 ---
hello, code in e.c is somethng like typedef struct { int a; } A; typedef struct { A * c[10]; } B; typedef struct { B * c[10]; } C; C v; /* one of the 3 contracts below (wth MAXLEN==10)*/ void foo(void); 3rd attempt below isnt an excepton: shouldit be also recorded as bug in bts? thanx for your help jc 2009/9/25, Julien Signoles <Julien.Signoles at cea.fr>: > > 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 > > _______________________________________________ > 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 > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090925/d171a607/attachment.htm