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?

Suppose I have a subprogram written using the SPARK Ada subset with postconditions verifying some property - for example, that the returned array is sorted, whose body just calls out to a function external to SPARK - for example, a C/C++ function that sorts arrays. Is there any way to force SPARK to assume, after this call, that the array will be sorted?