[eacsl] Update comparison translation to correctly not support structs and unions

src/plugins/e-acsl/src/code_generator/logic_array.ml

@@ -32,25 +32,6 @@ let translate_rte_ref:
   in
   ref func
 
-(** @return the content of the array type if [ty] is an array, or None
-    otherwise. *)
-let rec get_array_typ_opt ty =
-  if Gmp_types.is_t ty then
-    (* GMP pointer types are declared as arrays of one element. They are treated
-       as a special case here to ensure that they are not considered as arrays.
-    *)
-    None
-  else
-    match ty with
-    | TNamed (r, _) -> get_array_typ_opt r.ttype
-    | TArray (t, eo, bsot, a) -> Some (t, eo, bsot, a)
-    | _ -> None
-
-let is_array ty =
-  match get_array_typ_opt ty with
-  | Some _ -> true
-  | None -> false
-
 (** Retrieve the length of the [array] expression in a new variable [name] and
     return it as an expression.
     If the length is present in the type then the function directly assigns the
@@ -58,7 +39,7 @@ let is_array ty =
     [length = (\block_length(array) - \offset(array)) / sizeof(elem_typ)]. *)
 let length_exp ~loc kf env ~name array =
   let elem_typ, array_len =
-    match get_array_typ_opt (Cil.typeOf array) with
+    match Logic_aggr.get_array_typ_opt (Cil.typeOf array) with
     | None -> Options.fatal "Trying to retrieve the length of a non-array"
     | Some (t, len, _, _) -> t, len
   in

src/plugins/e-acsl/src/code_generator/logic_array.mli

@@ -22,9 +22,6 @@
 
 open Cil_types
 
-val is_array: typ -> bool
-(** @return true iff the type is an array *)
-
 val comparison_to_exp: loc:location -> kernel_function -> Env.t ->
   name:string -> binop -> exp -> exp -> exp * Env.t
 (** [comparison_to_exp ~loc kf env ~name bop e1 e2] generate the C code

src/plugins/e-acsl/src/code_generator/translate.ml

@@ -788,8 +788,8 @@ and comparison_to_exp
   let ty1 = Cil.typeOf e1 in
   let e2, env = term_to_exp kf env t2 in
   let ty2 = Cil.typeOf e2 in
-  match Logic_array.is_array ty1, Logic_array.is_array ty2 with
-  | true, true ->
+  match Logic_aggr.get_t ty1, Logic_aggr.get_t ty2 with
+  | Logic_aggr.Array, Logic_aggr.Array ->
     Logic_array.comparison_to_exp
       ~loc
       kf
@@ -798,7 +798,9 @@ and comparison_to_exp
       bop
       e1
       e2
-  | false, false -> (
+  | Logic_aggr.StructOrUnion, Logic_aggr.StructOrUnion ->
+    Env.not_yet env "comparison between two structs or unions"
+  | Logic_aggr.NotAggregate, Logic_aggr.NotAggregate -> begin
       match ity with
       | Typing.C_integer _ | Typing.C_float _ | Typing.Nan ->
         Cil.mkBinOp ~loc bop e1 e2, env
@@ -822,10 +824,13 @@ and comparison_to_exp
         Rational.cmp ~loc bop e1 e2 env kf t_opt
       | Typing.Real ->
         Error.not_yet "comparison involving real numbers"
-    )
+    end
   | _, _ ->
-    Options.fatal ~current:true "Comparison involving an array with something \
-                                 else."
+    Options.fatal
+      ~current:true
+      "Comparison involving incompatible types: '%a' and '%a'"
+      Printer.pp_typ ty1
+      Printer.pp_typ ty2
 
 and at_to_exp_no_lscope env kf t_opt label e =
   let stmt = E_acsl_label.get_stmt kf label in