Result attached or exception

Question

Let's say that I have a function f which should return an attached T by calling g. However, g returns a detachable T. If g results in a Void, I want to raise an exception like this:

f: T
  do
    if attached g as res then
      Result := res
    else
      raise
    end
  end
  
raise
  do
    (create {DEVELOPER_EXCEPTION}).raise
  end

In this setup EiffelStudio gives me an error VEVI: Variable is not properly set. Variable: Result at the end of f.

Indeed, Result can be Void at the end of f but the execution should not reach the end of f in this case, an exception should have been raised.

How can I restructure the code to achieve a similar result?

Answer 1

If the type of a raised exception does not matter, the following code will do:

f: T
    do
        Result := g
        check is_g_attached: attached Result then end
    end

If the type of the raised exception is important, the feature raise can be augmented with the postcondition False that indicates that the feature never returns. Then, the code would look like

f: T
    do
        Result := g
        if not attached Result then
            raise
        end
    end

raise
    do
        (create {DEVELOPER_EXCEPTION}).raise
    ensure
        False
    end