Having problem with SPARK Ada complaining that 'No EXPRESSION can start with reserved word "OTHERS".'

Having problem with SPARK Ada complaining that 'No EXPRESSION can start with reserved word "OTHERS".'

[Ben Hocking]

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!

Re: Having problem with SPARK Ada complaining that 'No EXPRESSION can start with reserved word "OTHERS".'

[Phil Thornley]

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

Re: Having problem with SPARK Ada complaining that 'No EXPRESSION can start with reserved word "OTHERS".'

[Ben Hocking]

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

Re: Having problem with SPARK Ada complaining that 'No EXPRESSION can start with reserved word "OTHERS".'

[roderick.chapman]

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

Re: Having problem with SPARK Ada complaining that 'No EXPRESSION can start with reserved word "OTHERS".'

[Ludovic Brenta]

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.