Description:
------------
In PHP 5.3.X, passing a null byte as decimal point lead to no decimal point at 
all. This is not so much problematic for userland, as for C extensions. For 
examlpe phpredis uses it internally (see 
https://github.com/nicolasff/phpredis/blob/master/redis.c#L3665) to format a 
number. This worked fine in PHP 5.3, but with PHP 5.4 only the first character 
until the first decimal point is returned.

Test script:
---------------
php -r 'var_dump(number_format(2000.1, 0, ".", "\x00"));'

Expected result:
----------------
string(4) "2000"

Actual result:
--------------
string(1) "2"