-
Notifications
You must be signed in to change notification settings - Fork 0
Return Statement
The return statement terminates the execution of function, optionally setting the return parameters of the function.
It has two forms, parameterless and parametric.
The parametric form consists of the keyword return followed by comma-separated list of expressions.
The number and types of expressions must match the declared return parameters of the function (matching of types is with respect to the assignability relation). This is the same as assigning all of the return parameters immediately before a parameterless return.
The parameterless form is just the keyword
return
This is equivalent to
return retarg1, retarg2, retarg3
where the arguments are the names of all the return parameters as declared in the function header.
The return statement always terminates execution of the function. Any statements that sequentially follow after a return are dead code. The state immediately after the return statement must satisfy the postconditions of the function.
If the return occurs in a statements with associated cleanup, the cleanup is performed after assigning the return parameters.
Successful static analysis requires that every path that ends in a parameterless return has already assigned all of the return parameters.
If there is no return statement at the end of the main function block, this is the same as if a parameterless return was present as the last statement of the block.