benchmark for php_strip_whitespace

benchmark_php_strip_whitespace.php

<?php

$i = 5000;
$t = start_test();

while($i--){
  php_strip_whitespace(__FILE__);
}

end_test($t, 'total');

//following utils copy from Zend/bench.php
function getmicrotime()
{
  $t = gettimeofday();
  return ($t['sec'] + $t['usec'] / 1000000);
}

function start_test()
{
	ob_start();
  return getmicrotime();
}

function end_test($start, $name)
{
  global $total;
  $end = getmicrotime();
  ob_end_clean();
  $total += $end-$start;
  $num = number_format($end-$start,3);
  $pad = str_repeat(" ", 24-strlen($name)-strlen($num));

  echo $name.$pad.$num."\n";
	ob_start();
  return getmicrotime();
}

@jhdxr Have you considered to use hrtime()?