--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on October 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] using logic type for struct with Frama-C Oxygen



Hello St?phane,

2012/10/17 DUPRAT Stephane <stephane.duprat at atos.net>:
> Can we presume that logic types are out of the scope of Oxygen ?
>
> De : frama-c-discuss-bounces at lists.gforge.inria.fr
> [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de DUPRAT

> I?m trying to use a logic type struct following the example 2.12 of [ACSL
> Version 1.6 Implementation in Oxygen-20120901] with the new release Frama-C
> Oxygen.
>
>
>
> //@ type point = struct { real x; real y; };
>
> //@ logic point origin = { .x = 0.0 , .y = 0.0 };
>

Sorry, we should have answered earlier. You're right, logic record
type are not supported in Oxygen (see figure 2.16 on page 51 of the
implementation manual). As a matter of fact, there's no distinction
between supported and unsupported examples in the manual. This is
mentionned only in the BNF grammar..

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile