--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on June 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Aggregate Logic Types



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