SPARK: missing case value

[Maciej Sobczak <see.my.homepage@gmail.com>]

Consider:

   type Enum is (A, B, C);

   procedure Test (E : in Enum)
      with Pre => E /= C
   is
   begin
      case E is
         when A => null;
         when B => null;
      end case;
   end Test;

The Pre contract says that C is never used as a value for E. Still, GNATProve complains about missing case value C in the case statement. The compiler complains, too.

An appropriate subtype (subtype SEnum is Enum range A .. B) can solve this, but it shows some asymmetry between subtypes and contracts, where I would expect that the same subsetting effect can be achieved in both ways. Apparently (and according to AARM), the case statement does not take contracts into account, but my understanding of the rules is that it would not be against the spirit of "covering values that satisfy the predicate".

On the other hand, SPARK is supposed to be a subset of Ada, so even if the above is feasible from the SPARK point of view, it should compile as regular Ada as well and compilers are not required to do this level of static analysis. So, SPARK does not do it, because Ada might not be able to keep the pace.

What are your thoughts on this?

-- 
Maciej Sobczak * http://www.inspirel.com