--- layout: fc_discuss_archives title: Message 61 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)?

many thnx for any help,
jc