--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on September 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] requires on arrays and strct



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