diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml index 0ceb31ebeffbe58188a5b190fd90e44cdce32564..1eea5272392cc68d53930ff6d18792a6fa772ce0 100644 --- a/src/plugins/e-acsl/src/analyses/typing.ml +++ b/src/plugins/e-acsl/src/analyses/typing.ml @@ -949,8 +949,8 @@ let get_cast ~lenv t = try Option.map typ_of_number_ty info.cast with Not_a_number -> None -let get_cast_of_predicate p = - let info = type_predicate p in +let get_cast_of_predicate ~lenv p = + let info = type_predicate ~lenv p in try Option.map typ_of_number_ty info.cast with Not_a_number -> assert false diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli index ac869b8770cb12f32487c5873c0ec4570fb00a49..e56f54b73e9067ce9eea0575a90ffe3378248625 100644 --- a/src/plugins/e-acsl/src/analyses/typing.mli +++ b/src/plugins/e-acsl/src/analyses/typing.mli @@ -138,7 +138,7 @@ val get_op: lenv:Function_params_ty.t -> term -> typ val get_cast: lenv:Function_params_ty.t -> term -> typ option (** Get the type which the given term must be converted to (if any). *) -val get_cast_of_predicate: predicate -> typ option +val get_cast_of_predicate: lenv:Function_params_ty.t -> predicate -> typ option (** Like {!get_cast}, but for predicates. *) val unsafe_set: term -> ?ctx:number_ty -> number_ty -> unit diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml index 246079281d9df8a1cf93202cf67a004a4907b35e..ad07712f4dc21a38dd2f1f2447d5911acd6611c1 100644 --- a/src/plugins/e-acsl/src/code_generator/translate.ml +++ b/src/plugins/e-acsl/src/code_generator/translate.ml @@ -1234,7 +1234,11 @@ and predicate_to_exp ~adata ?name kf ?rte env p = predicate_content_to_exp ~adata ?name kf env p in let env = if rte then translate_rte kf env e else env in - let cast = Typing.get_cast_of_predicate p in + let cast = + Typing.get_cast_of_predicate + ~lenv:(Env.Local_vars.get env) + p + in Extlib.nest adata (Typed_number.add_cast