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] using logic type for struct with Frama-C Oxygen

  • Subject: [Frama-c-discuss] using logic type for struct with Frama-C Oxygen
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Wed, 17 Oct 2012 15:00:28 +0200
  • In-reply-to: <569C6D7D26484241A530B87F45ADE1F80CA2C07E@AOFRWMBXRSC004.resources.atosorigin.local>
  • References: <569C6D7D26484241A530B87F45ADE1F80CA0BC8A@AOFRWMBXRSC004.resources.atosorigin.local> <569C6D7D26484241A530B87F45ADE1F80CA2C07E@AOFRWMBXRSC004.resources.atosorigin.local>
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