* Having problem with SPARK Ada complaining that 'No EXPRESSION can start with reserved word "OTHERS".'
@ 2012-06-14 12:43 Ben Hocking
2012-06-14 13:37 ` Phil Thornley
2012-06-14 13:41 ` Ludovic Brenta
0 siblings, 2 replies; 5+ messages in thread
From: Ben Hocking @ 2012-06-14 12:43 UTC (permalink / raw)
The following is a simple test program to demonstrate the issue.
test.ads:
====
package Test is
type QState is (Off, On, Both);
subtype Z4 is Integer range 0 .. 3; -- 0, 1, 2, or 3
type Ensemble is array (Z4) of QState;
procedure Foo;
end Test;
====
test.adb:
====
package body Test is
procedure Foo
is
SomeQState : Ensemble := (others => Off);
begin
null;
end Foo;
end Test;
====
When I use SPARK->Examine File (from GPS), I get the following message:
4:33 Syntax Error No EXPRESSION can start with reserved word "OTHERS".
I get the same error if I type "spark test.adb" from the terminal window (I'm on Mac OS X 10.6.8).
I know this is valid Ada, because this compiles without issue:
gcc -c -g -gnatQ -gnato -fstack-check -g test.adb
I've tried this with both SPARK95 and SPARK2005. I'm using the AdaCore tool chain. The version information for SPARK is:
$ spark -version
*******************************************************
Examiner GPL 2011
Copyright (C) 2011 Altran Praxis Limited, Bath, U.K.
*******************************************************
Any help would be appreciated!
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Having problem with SPARK Ada complaining that 'No EXPRESSION can start with reserved word "OTHERS".'
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 13:41 ` Ludovic Brenta
1 sibling, 1 reply; 5+ messages in thread
From: Phil Thornley @ 2012-06-14 13:37 UTC (permalink / raw)
In article <a3be9ddf-413a-475d-839c-6994473df43a@googlegroups.com>,
benjaminhocking@gmail.com says...
>
> The following is a simple test program to demonstrate the issue.
> test.ads:
In SPARK all aggregates must be qualified with the type:
SomeQState : Ensemble := Ensemble'(others => Off);
This isn't particularly clear in any of the documentation, but see
Section 4.3 of the SPARK LRM or page 110 of the book (High Integrity
Software by John Barnes).
Cheers,
Phil
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Having problem with SPARK Ada complaining that 'No EXPRESSION can start with reserved word "OTHERS".'
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:41 ` Ludovic Brenta
1 sibling, 0 replies; 5+ messages in thread
From: Ludovic Brenta @ 2012-06-14 13:41 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Having problem with SPARK Ada complaining that 'No EXPRESSION can start with reserved word "OTHERS".'
2012-06-14 13:37 ` Phil Thornley
@ 2012-06-14 13:49 ` Ben Hocking
2012-06-14 21:48 ` roderick.chapman
0 siblings, 1 reply; 5+ messages in thread
From: Ben Hocking @ 2012-06-14 13:49 UTC (permalink / raw)
Cc: phil.jpthornley
On Thursday, June 14, 2012 9:37:43 AM UTC-4, Phil Thornley wrote:
> In SPARK all aggregates must be qualified with the type:
>
> SomeQState : Ensemble := Ensemble'(others => Off);
Thanks, Phil. That fixed the problem in both my sample code and my real code. (In the sample code, many other warnings were then generated, but they all made perfect sense to me.)
-Ben
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Having problem with SPARK Ada complaining that 'No EXPRESSION can start with reserved word "OTHERS".'
2012-06-14 13:49 ` Ben Hocking
@ 2012-06-14 21:48 ` roderick.chapman
0 siblings, 0 replies; 5+ messages in thread
From: roderick.chapman @ 2012-06-14 21:48 UTC (permalink / raw)
Cc: phil.jpthornley
Ben,
In the documents that come with the GPL edition, see section 4.3 of SPARK_LRM.pdf - the rules
are clearly stated there.
- Rod Chapman, SPARK Team
^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2012-06-14 22:55 UTC | newest]
Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
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 is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox