"int" is not a suitable type to convert time()'s return value to. Avoid
casts and other extra fiddling by using difftime(), on the assumption
that the overhead of using "double" doesn't matter here.
Coverity ID: 1509374
Signed-off-by: Jan Beulich <jbeulich@suse.com>
Reviewed-by: Anthony PERARD <anthony.perard@citrix.com>