How to mark unreachable code in Ada/SPARK

Question

I have the following code:

   function Linear_Search (A : Elem_Array; E : Elem) return Index is
   begin
      for i in A'Range loop
         pragma Loop_Invariant (for some J in i .. A'Last => A (J) = E);
         if A (i) = E then
            return i;
         end if;
      end loop;
      return A'Last;
   end Linear_Search;

This function has a precondition that says that the array contains the element searched for:

   function Contains (A : Elem_Array; E : Elem) return Boolean is
     (for some I in A'Range => A (I) = E);

   function Linear_Search (A : Elem_Array; E : Elem) return Index with
      Pre  => Contains (A, E),
      Post => A (Linear_Search'Result) = E;

So I would like to remove the return statement after the loop, or at least mark it as unreachable for clarity; is there any way to do that such that the compiler can also use that to optimize? What is the recommended way to mark unreachable code in Ada/SPARK?

Answer 1

You can prove a particular code section to be unreachable by raising an exception in that section on purpose. As GNATprove tries to prove the absence of runtime errors in general, it will try to prove that the explicit exception will never be raised. The only way it can prove that an explicit exception will never be raised, is by proving that the particular code section is unreachable.

So, in your particular example, just replace the return statement with a raise statement.

function Linear_Search (A : Elem_Array; E : Elem) return Index is
begin      
   for i in A'Range loop
      pragma Loop_Invariant (for some J in i .. A'Last => A (J) = E);
      if A (i) = E then
         return i;
      end if;
   end loop;      
   raise Program_Error with "unreachable"; 
end Linear_Search;

SPARK will prove that the exception will never be raised because the code is unreachable:

info: raise statement or expression proved unreachable (CVC4: 1 VC)

Answer 2

You can eliminate the first return statement entirely, leaving only the second return statement:

   function Linear_Search (A : Elem_Array; E : Elem) return Index is
       Result : Index := A'Last;
   begin
      for i in A'Range loop
         pragma Loop_Invariant (for some J in i .. A'Last => A (J) = E);
         if A (i) = E then
            Result := i;
            exit;
         end if;
      end loop;
      return Result;
   end Linear_Search;