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] Aggregate Logic Types

  • Subject: [Frama-c-discuss] Aggregate Logic Types
  • From: frank at dordowsky.de (Frank Dordowsky)
  • Date: Thu, 19 Jun 2014 17:14:50 +0200 (CEST)
Is it possible to declare logic aggregate types using C types? The
implementation notes (ACSL Version 1.7 Implementation in
Fluorine-20130601) seem to indicate that it is possible, but I get a
parsing error when I try the following

/*@ type t_larray = int[3];
     logic t_larray larr = {1,2,3}; 
*/

If this is not possible, are ghost arrays a good work-around? I try to use 
constant arrays to define a piecewise linear logic function.
Thanks in advance 
Frank