Hi Jaak,
A goto to the "Error" label is supposed to be executed when execution
reaches the end of a procedure without finding a return statement. I
suspect that in this case, the return is returning to someplace that
drops it off the end of a calling procedure. I can't tell exactly
what's happening without seeing a complete example. If you have an
example in which such a goto is being executed when it shouldn't be,
please send it to me. (But please try to pare it down to the smallest
example you can find.)
The translator does not produce an error because it doesn't know
whether that goto "Error" can actually be executed. Determining
whether a particular statement in a program will be executed is an
unsolvable problem, and we had more important things to do than add
heuristics to the translator for attempting to solve this problem.
It is good practice to always have TLC check a type invariant. A type
invariant that is false when pc equals "Error" will catch that error
when it occurs.
Best regards,
Leslie