Skip to content
Snippets Groups Projects
Commit e283b28e authored by Jan Rochel's avatar Jan Rochel
Browse files

[e-acsl] Translate_utils: cut comparison_to_exp into two

parent c3a97b1e
No related branches found
No related tags found
No related merge requests found
...@@ -169,29 +169,9 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t = ...@@ -169,29 +169,9 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
let () = let () =
Memory_translate.gmp_to_sizet_ref := gmp_to_sizet Memory_translate.gmp_to_sizet_ref := gmp_to_sizet
let comparison_to_exp let exp_comparison_to_exp
~adata ~loc kf env ity bop e1 e2 ?(name = Misc.name_of_binop bop) t_opt =
~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 ty1 = Cil.typeOf e1 in 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 ty2 = Cil.typeOf e2 in
let e, env = let e, env =
match Logic_aggr.get_t ty1, Logic_aggr.get_t ty2 with match Logic_aggr.get_t ty1, Logic_aggr.get_t ty2 with
...@@ -221,6 +201,20 @@ let comparison_to_exp ...@@ -221,6 +201,20 @@ let comparison_to_exp
Printer.pp_typ ty1 Printer.pp_typ ty1
Printer.pp_typ ty2 Printer.pp_typ ty2
in 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 e, adata, env
let conditional_to_exp ?(name="if") ~loc kf t_opt e1 (e2, env2) (e3, env3) = let conditional_to_exp ?(name="if") ~loc kf t_opt e1 (e2, env2) (e3, env3) =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment