diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml index 4bf408a33b67d80ff6fb21f50c40896dfcdda8cd..8f262208a12b8bd78a5709aa18e15147f86eaafa 100644 --- a/src/plugins/e-acsl/interval.ml +++ b/src/plugins/e-acsl/interval.ml @@ -53,8 +53,8 @@ module D = Ival.compare i1 i2 | Float (k1, f1), Float (k2, f2) -> (* faster to compare a kind than a float *) - let n = Stdlib.compare k1 k2 in - if n = 0 then Stdlib.compare f1 f2 else n + let n = Transitioning.Stdlib.compare k1 k2 in + if n = 0 then Transitioning.Stdlib.compare f1 f2 else n | Ival _, (Float _ | Rational | Real | Nan) | Float _, (Rational | Real | Nan) | Rational, (Real | Nan) @@ -92,7 +92,7 @@ module D = let is_included i1 i2 = match i1, i2 with | Ival i1, Ival i2 -> Ival.is_included i1 i2 | Float(k1, f1), Float(k2, f2) -> - Stdlib.compare k1 k2 <= 0 + Transitioning.Stdlib.compare k1 k2 <= 0 && (match f1, f2 with | None, None | Some _, None -> true | None, Some _ -> false @@ -125,7 +125,7 @@ let lift_binop ~safe_float f i1 i2 = match i1, i2 with | Ival i1, Ival i2 -> Ival (f i1 i2) | Float(k1, _), Float(k2, _) when safe_float -> - let k = if Stdlib.compare k1 k2 >= 0 then k1 else k2 in + let k = if Transitioning.Stdlib.compare k1 k2 >= 0 then k1 else k2 in Float(k, None (* lost value, if any before *)) | Ival iv, Float(k, _) | Float(k, _), Ival iv -> diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml index 8abc13fd1cbfcffe19254939ee5fff78a29ee12c..2e38092451762ce6bc5cb878d38acb095e4fa1b4 100644 --- a/src/plugins/e-acsl/typing.ml +++ b/src/plugins/e-acsl/typing.ml @@ -67,7 +67,7 @@ module D = if i1 = i2 then 0 else if Cil.intTypeIncluded i1 i2 then -1 else 1 | C_float f1, C_float f2 -> - Stdlib.compare f1 f2 + Transitioning.Stdlib.compare f1 f2 | (C_integer _ | C_float _ | Gmpz | Rational | Real), Nan | (C_integer _ | C_float _ | Gmpz | Rational ), Real | (C_integer _ | C_float _ | Gmpz), Rational