#4 may insert unreachable code

[Suran]

for post-conditions in methods returning void a check
for it is inserted as the last statement (and on all
return-statements), this place may be unreachable.

A Full program-flow-analysis needs to be written to
know if this happenes or the original method be
replaced by a wrapper-method.