The type checker function Uty2Stmt produces a struct TypeInfo with the following attributes:

• msgs is a list of messages that is empty if the type-checking was successful, and contains otherwise messages to report the type errors.
• lblL is the list of control flow labels in the typed statement (note that new labels can be generated due to unrolling of generic statements).
• lcVL contains the declarations of the declared local variables (note again that new local variables may be generated by unroling of generic statements).
• lcNL contains the names of assertions, assumptions etc.
• orcL contains the declarations of introduced oracle variables used to replace nondeterministic statements.
• stmt finally is the generated typed statement.