Long ago I integrated Herbie with the Clang Static Analyzer to process floating point expressions and warn about avoidable accuracy loss. The neat thing was tha

Long ago I integrated Herbie with the Clang Static Analyzer to process floating point expressions and warn about avoidable accuracy loss. The neat thing was that it could deal with loops, calculations split across multiple assignments, etc. But I never came up with a heuristic for knowing when the calculation was "complete" so it generated too many intermediate warnings.