Static bounds of loop - compilation error

Static bounds of loop - compilation error

[pascal.malaise]

Hi Ada experts,

can anyone explain the following compilation errors:
procedure T is
  type E is (A, B, C);
  subtype S is E range A .. B;
  X, Y : S;
begin
  X := A;
  Y := B;
  for I in S range X .. Y loop
    case I is
      when A => null;
      when B => null;
    end case;
  end loop;
end T;
>> missing case value: "C"

A similar example where S is a subtype of Positive leads to the same  error and also: bounds of "I" are not static, alternatives must cover base type

Indeed, X and Y are not static but the bounds of S are, and all the values of S are covered in the "case".

So is it a bug?

Thank you

Re: Static bounds of loop - compilation error

[Georg Bauhaus]

On 30.10.12 14:26, pascal.malaise@gmail.com wrote:
> Hi Ada experts,
> 
> can anyone explain the following compilation errors:
> procedure T is
>   type E is (A, B, C);
>   subtype S is E range A .. B;
>   X, Y : S;
> begin
>   X := A;
>   Y := B;
>   for I in S range X .. Y loop
>     case I is
>       when A => null;
>       when B => null;
>     end case;
>   end loop;
> end T;
>>> missing case value: "C"

> So is it a bug?

I won't speculate, but assuming it is not a bug, then qualifying the I
should not make the compiler think the source is fine after qualifying?

 for I in S range X .. Y loop
    case S'(I) is
      when A => null;
      when B => null;
    end case;
  end loop;

Re: Static bounds of loop - compilation error

[Adam Beneschan]

On Tuesday, October 30, 2012 6:26:09 AM UTC-7, pascal....@gmail.com wrote:
> Hi Ada experts,
> 
> can anyone explain the following compilation errors:
> 
> procedure T is
>   type E is (A, B, C);
>   subtype S is E range A .. B;
>   X, Y : S;
> begin
>   X := A;
>   Y := B;
>   for I in S range X .. Y loop
>     case I is
>       when A => null;
>       when B => null;
>     end case;
>   end loop;
> end T;
> 
> >> missing case value: "C"
> 
> A similar example where S is a subtype of Positive leads to the same  error and also: bounds of "I" are not static, alternatives must cover base type
> 
> Indeed, X and Y are not static but the bounds of S are, and all the values of S are covered in the "case".
> 
> So is it a bug?

No.  RM 5.4 gives three rules for how the values of a CASE must be covered, based on the "nominal subtype" of the expression (in this case, the name I).  If the subtype is static and constrained, then everything in the subtype has to be covered; otherwise, everything in the *base range* has to be covered.  (The third rule has to do with universal integers and doesn't apply here.)  Here, I's subtype is not static, so therefore that rule doesn't apply, and the only rule left is the rule that everything in the base range has to be covered--which means everything in E.  There aren't any rules to handle a case like you've coded, where I's subtype is non-static but there's another subtype involved (because if the "S" in "S range X .. Y"); I think that adding language rules for this would mean that I has yet another kind of subtype associated with it, in addition to the "actual" and "nominal" subtypes, which would probably make things too complicated.

Saying either

  case S(I) is

or

  case S'(I) is

should make things work, because now the CASE expression has a nominal subtype S, which is static, rather than "S range X .. Y", which isn't.

                         -- Adam

Re: Static bounds of loop - compilation error

[Yannick Duchêne (Hibou57)]

Le Tue, 30 Oct 2012 17:10:54 +0100, Adam Beneschan <adam@irvine.com> a  
écrit:
>   case S(I) is
>
> or
>
>   case S'(I) is
>
> should make things work, because now the CASE expression has a nominal  
> subtype S, which is static, rather than "S range X .. Y", which isn't.
>
>                          -- Adam

That indeed solve the issue.

Note that you can also declare the type at the iteration variable too, a  
good practice, which is even mandatory with SPARK. Unfortunately, doing  
this, ends in a GNAT bug‑box:

     procedure T is
        type E is (A, B, C);
        subtype S is E range A .. B;
        X, Y : S;
     begin
        X := A;
        Y := B;
        for I : S in X .. Y loop
           case I is
              when A => null;
              when B => null;
           end case;
        end loop;
     end T;

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Static bounds of loop - compilation error

[Yannick Duchêne (Hibou57)]

Le Tue, 30 Oct 2012 18:03:38 +0100, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> Note that you can also declare the type at the iteration variable too, a  
> good practice, which is even mandatory with SPARK. Unfortunately, doing  
> this, ends in a GNAT bug‑box:
>
>      procedure T is
>         type E is (A, B, C);
>         subtype S is E range A .. B;
>         X, Y : S;
>      begin
>         X := A;
>         Y := B;
>         for I : S in X .. Y loop
>            case I is
>               when A => null;
>               when B => null;
>            end case;
>         end loop;
>      end T;

Oops, sorry, I'm buggy. That's erroneous, the syntax is not good. I don't  
know why GNAT gives a bug box instead. That's only `for I in S range X ..  
Y loop` as in the original message.


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Static bounds of loop - compilation error

[Marc C]

On Tuesday, October 30, 2012 12:15:37 PM UTC-5, Hibou57 (Yannick Duchêne) wrote:

> Oops, sorry, I'm buggy. That's erroneous, the syntax is not good. I don't  
> know why GNAT gives a bug box instead.

You get a bug box because there's a bug in the GNAT compiler. That isn't the first bug that's shown up in GNAT GPL 2012's with regard to Ada 2012 features.

Report it to report@AdaCore.com!

Marc A. Criley

Re: Static bounds of loop - compilation error

[pascal.malaise]

Thank you for the explaination.