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?
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