From 3441230f92556f796424092ced5c3392bb47d00a Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 10 Jun 2020 17:07:54 +0200
Subject: [PATCH] [eacsl] Add support for logic arrays in
`Translate.comparison_to_exp`
---
.../e-acsl/src/code_generator/translate.ml | 64 ++++++++++++-------
1 file changed, 41 insertions(+), 23 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index b7d70865560..b9dfc2390c4 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -762,29 +762,46 @@ and comparison_to_exp
| Some e1 ->
e1, env
in
+ let ty1 = Cil.typeOf e1 in
let e2, env = term_to_exp kf env t2 in
- match ity with
- | Typing.C_integer _ | Typing.C_float _ | Typing.Nan ->
- Cil.mkBinOp ~loc bop e1 e2, env
- | Typing.Gmpz ->
- let _, e, env = Env.new_var
- ~loc
- env
- kf
- t_opt
- ~name
- Cil.intType
- (fun v _ ->
- [ Constructor.mk_lib_call ~loc
- ~result:(Cil.var v)
- "__gmpz_cmp"
- [ e1; e2 ] ])
- in
- Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
- | Typing.Rational ->
- Rational.cmp ~loc bop e1 e2 env kf t_opt
- | Typing.Real ->
- Error.not_yet "comparison involving real numbers"
+ let ty2 = Cil.typeOf e2 in
+ match Logic_array.is_array ty1, Logic_array.is_array ty2 with
+ | true, true ->
+ Logic_array.comparison_to_exp
+ ~loc
+ kf
+ env
+ ~name
+ bop
+ e1
+ e2
+ | false, false -> (
+ match ity with
+ | Typing.C_integer _ | Typing.C_float _ | Typing.Nan ->
+ Cil.mkBinOp ~loc bop e1 e2, env
+ | Typing.Gmpz ->
+ let _, e, env = Env.new_var
+ ~loc
+ env
+ kf
+ t_opt
+ ~name
+ Cil.intType
+ (fun v _ ->
+ [ Constructor.mk_lib_call ~loc
+ ~result:(Cil.var v)
+ "__gmpz_cmp"
+ [ e1; e2 ] ])
+ in
+ Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
+ | Typing.Rational ->
+ Rational.cmp ~loc bop e1 e2 env kf t_opt
+ | Typing.Real ->
+ Error.not_yet "comparison involving real numbers"
+ )
+ | _, _ ->
+ Options.fatal ~current:true "Comparison involving an array with something \
+ else."
and at_to_exp_no_lscope env kf t_opt label e =
let stmt = E_acsl_label.get_stmt kf label in
@@ -1080,7 +1097,8 @@ let () =
Mmodel_translate.term_to_exp_ref := term_to_exp;
Mmodel_translate.predicate_to_exp_ref := named_predicate_to_exp;
Logic_functions.term_to_exp_ref := term_to_exp;
- Logic_functions.named_predicate_to_exp_ref := named_predicate_to_exp
+ Logic_functions.named_predicate_to_exp_ref := named_predicate_to_exp;
+ Logic_array.translate_rte_ref := translate_rte
(* This function is used by Guillaume.
However, it is correct to use it only in specific contexts. *)
--
GitLab