Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with array type in Frama-C

  • Subject: [Frama-c-discuss] Problem with array type in Frama-C
  • From: tienhm at gmail.com (Tien Hoang Minh)
  • Date: Mon, 20 Jul 2009 14:35:31 -0400
Hi everybody,
I always get an error message when using the array type with frama-c
(lithium), like in the following example

/*@ logic integer getelem(integer t[], integer i) = t[i];
  @*/

The error message is "not a C type"
Please help me if there is an error in my annotation or if it is a
feature not yet available in frama-c.
Thank you very much.
Tien.