--- layout: fc_discuss_archives title: Message 65 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,
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