Frama-C API - Float_interval
module Make (Float : Float_sig.S) : Float_interval_sig.S with type float := Float.tBuilds a semantics of floating-point intervals for different precisions, from a module providing the floating-point numbers used for the bounds of the intervals. Supports NaN and infinite values.