os: change CPU time from Integer to Number

CPU time values must be Numbers, not Integers, as they can be too large
for Integers on 32 bit platforms.