It is completely unrelated to run_time_clock, so I don't think it makes
sense to have it as a static function there.
Move it to be a free function named "get_run_time".
Change-Id: I0c3e4d3cc44ca37e523c94d72f7cd66add95645e
Approved-By: Tom Tromey <tom@tromey.com>