# Functions provided by the replayer debugger