remove-unused

[Stephen Weeks]

I am confused by the code in remove-unused.  I don't understand what
"doesTerminate" means.  You sometimes seem to use it to mean "must
terminate" and other times to mean "may terminate".  Which is it?

As evidence, I point to the fact that if a function contains a Return
statement, it is marked as "doesTerminate".  This corresponds to "may
terminate".  

But, in translating calls you eliminate a call if it does not side
effect, does not raise, and doesTerminate.  To me, this requires
the "must terminate" interpretation, and therefore seems wrong.

Clarification?