The contract says that you have to call the function with 0 <= f <= FLT_MAX. So if you call it with Nan, any infinity, or a negative number other than -0 (which

The contract says that you have to call the function with 0 <= f <= FLT_MAX. So if you call it with Nan, any infinity, or a negative number other than -0 (which happens to satisfy 0 <= f), you are using it outside its specifications. In that, it is like a standard library strlen(). It does not work if you pass it NULL because it's specified as accepting well-formed strings.