Re: SPARK: missing case value

[Mark Lorenzen <mark.lorenzen@gmail.com>]

On Friday, October 9, 2015 at 1:38:35 PM UTC+2, Maciej Sobczak wrote:
> 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?

I think it is logical and correct. How would a compiler be able to determine the range of E if your precondition was more complex?

I would change the case statement into something like this:

case E is
   when A => null;
   when B => null;
   when C => raise Impossible; -- or maybe Pragma Assert (False)
end case;

Note that you can use raise statements in SPARK as long as the program is still in SPARK i.e. the raise statement will never be executed.

Regards,

Mark L