From: Ludovic Brenta <ludovic@ludovic-brenta.org>
Subject: Re: Having problem with SPARK Ada complaining that 'No EXPRESSION can start with reserved word "OTHERS".'
Date: Thu, 14 Jun 2012 06:41:41 -0700 (PDT)
Date: 2012-06-14T06:41:41-07:00 [thread overview]
Message-ID: <b8611897-e627-4b79-81e8-1a793e505be7@q29g2000vby.googlegroups.com> (raw)
In-Reply-To: a3be9ddf-413a-475d-839c-6994473df43a@googlegroups.com
Ben Hocking writes on comp.lang.ada:
> SomeQState : Ensemble := (others => Off);
[...]
> 4:33 Syntax Error No EXPRESSION can start with reserved word "OTHERS".
[...]
> I know this is valid Ada, because this compiles without issue:
> gcc -c -g -gnatQ -gnato -fstack-check -g test.adb
AFAICT, this is legal Ada but not legal SPARK. You should rewrite
the initialization as:
SomeQState : Ensemble := (Z4'First .. Z4'Last => Off);
though I'm not sure what the exact rules of SPARK are in this
regard. Also, it may be possible and preferable to write
Z4'Range => Off instead.
--
Ludovic Brenta.
The reporting unit should interactively connect the dots; this is
why the group facilitates agreed-upon and parallel value creations.
prev parent reply other threads:[~2012-06-14 17:13 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-06-14 12:43 Having problem with SPARK Ada complaining that 'No EXPRESSION can start with reserved word "OTHERS".' Ben Hocking
2012-06-14 13:37 ` Phil Thornley
2012-06-14 13:49 ` Ben Hocking
2012-06-14 21:48 ` roderick.chapman
2012-06-14 13:41 ` Ludovic Brenta [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox