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
- References:
- [Frama-c-discuss] using logic type for struct with Frama-C Oxygen
- From: stephane.duprat at atos.net (DUPRAT Stephane)
- [Frama-c-discuss] using logic type for struct with Frama-C Oxygen
- From: stephane.duprat at atos.net (DUPRAT Stephane)
- [Frama-c-discuss] using logic type for struct with Frama-C Oxygen
- Prev by Date: [Frama-c-discuss] using logic type for struct with Frama-C Oxygen
- Next by Date: [Frama-c-discuss] Is there any method not to initalize all global variables while doing value analysis?
- Previous by thread: [Frama-c-discuss] using logic type for struct with Frama-C Oxygen
- Next by thread: [Frama-c-discuss] Some information on invariant needs
- Index(es):