How to mark unreachable code in Ada/SPARK
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?