Reasoning about floating point in real-world systems