diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml index 195ec761fbc852f58b598938483a5bfe882a0728..ebb85f3c6d53ba5a231b24d15f7e332f01bb8cec 100644 --- a/src/plugins/e-acsl/translate.ml +++ b/src/plugins/e-acsl/translate.ml @@ -84,7 +84,7 @@ let constant_to_exp ?(loc=Location.unknown) = function | LStr s -> Cil.new_exp ?loc (Const (CStr s)), false | LWStr s -> Cil.new_exp ?loc (Const (CWStr s)), false | LChr c -> Cil.new_exp ?loc (Const (CChr c)), false - | LReal((f, l, u), s) -> + | LReal {r_literal=s; r_nearest=f; r_lower=l; r_upper=u} -> if l <> u then Options.feedback ~current:true ~once:true "approximating a real number by a float";