diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml index acaec461509f23680eb3bc963ec788cad81ef30e..ef8b075abf9db5814cb4fe9c6ee6103f520ca900 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml +++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml @@ -169,29 +169,9 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t = let () = Memory_translate.gmp_to_sizet_ref := gmp_to_sizet -let comparison_to_exp - ~adata - ~loc - kf - env - ity - ?e1 - bop - t1 - t2 - ?(name = Misc.name_of_binop bop) - t_opt - = - let e1, adata, env = - match e1 with - | None -> - let e1, adata, env = term_to_exp ~adata kf env t1 in - e1, adata, env - | Some e1 -> - e1, adata, env - in +let exp_comparison_to_exp + ~loc kf env ity bop e1 e2 ?(name = Misc.name_of_binop bop) t_opt = let ty1 = Cil.typeOf e1 in - let e2, adata, env = term_to_exp ~adata kf env t2 in let ty2 = Cil.typeOf e2 in let e, env = match Logic_aggr.get_t ty1, Logic_aggr.get_t ty2 with @@ -221,6 +201,20 @@ let comparison_to_exp Printer.pp_typ ty1 Printer.pp_typ ty2 in + e, env + +let comparison_to_exp ~adata ~loc kf env ity ?e1 bop t1 t2 ?name t_opt + = + let e1, adata, env = + match e1 with + | None -> + let e1, adata, env = term_to_exp ~adata kf env t1 in + e1, adata, env + | Some e1 -> + e1, adata, env + in + let e2, adata, env = term_to_exp ~adata kf env t2 in + let e, env = exp_comparison_to_exp ~loc kf env ity bop e1 e2 ?name t_opt in e, adata, env let conditional_to_exp ?(name="if") ~loc kf t_opt e1 (e2, env2) (e3, env3) =