PHP: A replacement for the shamefully broken DateTime::getTimestamp

getTimestampWithFraction.php

	/**
	 * Problem: `DateTime::getTimestamp` returns **_`int`_**! Calculations such as the following
	 * are incorrect if the `DateTime` object includes fractions of seconds:
	 *
	 * ```php
	 * $durationSeconds = strval($endTime->getTimestamp() - $startTimestamp);
	 * ```
	 *
	 * `DateTime::diff` can subtract properly, but only under PHP 7.1.  (Curiously,
	 * `DateTime::getTimestamp` still returns `int` under PHP 7.1!)
	 *
	 * @param DateTime $aDateTime
	 * @return float
	 */
	function getTimestampWithFraction(DateTime $aDateTime) {
		// One or both `floatval` calls may be unnecessary, but it's better to be safe.
		return floatval($aDateTime->getTimestamp()) + floatval($aDateTime->format('.u'));
	}