From c9c5d089e46d7a9e3cf998ab9c6f9bd69913da5e Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Thu, 9 Jun 2022 09:54:45 +0200
Subject: [PATCH] [e-acsl] typing specific types moved to analyses_types
---
.../e-acsl/src/analyses/analyses_datatype.ml | 54 ++++++++++++++++
.../e-acsl/src/analyses/analyses_datatype.mli | 3 +
.../e-acsl/src/analyses/analyses_types.mli | 9 ++-
src/plugins/e-acsl/src/analyses/typing.ml | 62 +------------------
src/plugins/e-acsl/src/analyses/typing.mli | 11 +---
src/plugins/e-acsl/src/code_generator/gmp.ml | 36 +++++------
src/plugins/e-acsl/src/code_generator/libc.ml | 14 ++---
.../src/code_generator/logic_functions.ml | 13 ++--
.../e-acsl/src/code_generator/loops.ml | 6 +-
.../src/code_generator/memory_translate.ml | 8 +--
.../src/code_generator/translate_ats.ml | 18 +++---
.../src/code_generator/translate_terms.ml | 21 +++----
.../src/code_generator/translate_utils.ml | 22 +++----
.../src/code_generator/translate_utils.mli | 3 +-
14 files changed, 131 insertions(+), 149 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index 0a28d7a5467..449c92e448b 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -429,3 +429,57 @@ module LF_env
let replace li args_ival ival = LFProf.Hashtbl.replace tbl (li, args_ival) ival
end
+
+module Number_ty =
+ Datatype.Make_with_collections
+ (struct
+ type t = number_ty
+ let name = "E_ACSL.Typing.t"
+ let reprs = [ Gmpz; Real; Nan; C_integer IInt ]
+ include Datatype.Undefined
+
+ let compare ty1 ty2 =
+ if ty1 == ty2 then 0
+ else
+ match ty1, ty2 with
+ | C_integer i1, C_integer i2 ->
+ if i1 = i2 then 0
+ else if Cil.intTypeIncluded i1 i2 then -1 else 1
+ | C_float f1, C_float f2 ->
+ Stdlib.compare f1 f2
+ | (C_integer _ | C_float _ | Gmpz | Rational | Real), Nan
+ | (C_integer _ | C_float _ | Gmpz | Rational ), Real
+ | (C_integer _ | C_float _ | Gmpz), Rational
+ | (C_integer _ | C_float _), Gmpz
+ | C_integer _, C_float _ ->
+ -1
+ | (C_float _ | Gmpz | Rational | Real | Nan), C_integer _
+ | (Gmpz | Rational | Real | Nan), C_float _
+ | (Rational | Real | Nan), Gmpz
+ | (Real | Nan), Rational
+ | Nan, Real ->
+ 1
+ | Gmpz, Gmpz
+ | Rational, Rational
+ | Real, Real
+ | Nan, Nan ->
+ assert false
+
+ let equal = Datatype.from_compare
+
+ let hash = function
+ | C_integer ik -> 7 * Hashtbl.hash ik
+ | C_float fk -> 97 * Hashtbl.hash fk
+ | Gmpz -> 787
+ | Rational -> 907
+ | Real -> 1011
+ | Nan -> 1277
+
+ let pretty fmt = function
+ | C_integer k -> Printer.pp_ikind fmt k
+ | C_float k -> Printer.pp_fkind fmt k
+ | Gmpz -> Format.pp_print_string fmt "Gmpz"
+ | Rational -> Format.pp_print_string fmt "Rational"
+ | Real -> Format.pp_print_string fmt "Real"
+ | Nan -> Format.pp_print_string fmt "Nan"
+ end)
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 48feedf5ee0..19a8ffa8033 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
@@ -101,3 +101,6 @@ module LF_env : sig
val replace : logic_info -> Profile.t -> ival -> unit
end
+
+module Number_ty: Datatype.S_with_collections
+ with type t = number_ty
diff --git a/src/plugins/e-acsl/src/analyses/analyses_types.mli b/src/plugins/e-acsl/src/analyses/analyses_types.mli
index 148dff16a51..01fc71a0b64 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_types.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_types.mli
@@ -68,10 +68,17 @@ type annotation_kind =
| Variant
| RTE
-
type ival =
| Ival of Ival.t
| Float of fkind * float option (* a float constant, if any *)
| Rational
| Real
| Nan
+
+type number_ty =
+ | C_integer of ikind
+ | C_float of fkind
+ | Gmpz
+ | Rational
+ | Real
+ | Nan
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 038254859b1..954ca8c4c84 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -43,13 +43,7 @@ let pending_typing : (unit -> unit) Stack.t = Stack.create ()
(** Datatype and constructor *)
(******************************************************************************)
-type number_ty =
- | C_integer of ikind
- | C_float of fkind
- | Gmpz
- | Rational
- | Real
- | Nan
+module D = Number_ty
let ikind ik = C_integer ik
let c_int = ikind IInt
@@ -58,60 +52,6 @@ let fkind fk = C_float fk
let rational = Rational
let nan = Nan
-module D =
- Datatype.Make_with_collections
- (struct
- type t = number_ty
- let name = "E_ACSL.Typing.t"
- let reprs = [ Gmpz; Real; Nan; c_int ]
- include Datatype.Undefined
-
- let compare ty1 ty2 =
- if ty1 == ty2 then 0
- else
- match ty1, ty2 with
- | C_integer i1, C_integer i2 ->
- if i1 = i2 then 0
- else if Cil.intTypeIncluded i1 i2 then -1 else 1
- | C_float f1, C_float f2 ->
- Stdlib.compare f1 f2
- | (C_integer _ | C_float _ | Gmpz | Rational | Real), Nan
- | (C_integer _ | C_float _ | Gmpz | Rational ), Real
- | (C_integer _ | C_float _ | Gmpz), Rational
- | (C_integer _ | C_float _), Gmpz
- | C_integer _, C_float _ ->
- -1
- | (C_float _ | Gmpz | Rational | Real | Nan), C_integer _
- | (Gmpz | Rational | Real | Nan), C_float _
- | (Rational | Real | Nan), Gmpz
- | (Real | Nan), Rational
- | Nan, Real ->
- 1
- | Gmpz, Gmpz
- | Rational, Rational
- | Real, Real
- | Nan, Nan ->
- assert false
-
- let equal = Datatype.from_compare
-
- let hash = function
- | C_integer ik -> 7 * Hashtbl.hash ik
- | C_float fk -> 97 * Hashtbl.hash fk
- | Gmpz -> 787
- | Rational -> 907
- | Real -> 1011
- | Nan -> 1277
-
- let pretty fmt = function
- | C_integer k -> Printer.pp_ikind fmt k
- | C_float k -> Printer.pp_fkind fmt k
- | Gmpz -> Format.pp_print_string fmt "Gmpz"
- | Rational -> Format.pp_print_string fmt "Rational"
- | Real -> Format.pp_print_string fmt "Real"
- | Nan -> Format.pp_print_string fmt "Nan"
- end)
-
(******************************************************************************)
(** Basic operations *)
(******************************************************************************)
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index a9be9966bbb..2fbf5e238a5 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -45,22 +45,13 @@
safely be computed in [int]: its result belongs to [[-2;4]]. *)
open Cil_types
+open Analyses_types
open Analyses_datatype
(******************************************************************************)
(** {2 Datatypes} *)
(******************************************************************************)
-(** Possible types infered by the system. *)
-
-type number_ty = private
- | C_integer of ikind
- | C_float of fkind
- | Gmpz
- | Rational
- | Real
- | Nan
-
(** {3 Smart constructors} *)
val c_int: number_ty
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index b2eec285b37..efc72c375b0 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Analyses_types
module Error = Translation_error
(**************************************************************************)
@@ -70,31 +71,24 @@ let get_set_suffix_and_arg res_ty e =
end
in
match (exp_number_ty, res_number_ty) with
- | Typing.Gmpz, Typing.Gmpz | Typing.Rational, Typing.Rational ->
- "", [ e ]
- | Typing.Gmpz, Typing.Rational ->
- "_z", [ e ]
- | Typing.Rational, Typing.Gmpz ->
- "_q", [ e ]
- | Typing.C_integer IChar, _ ->
+ | Gmpz, Gmpz | Rational, Rational -> "", [ e ]
+ | Gmpz, Rational -> "_z", [ e ]
+ | Rational, Gmpz -> "_q", [ e ]
+ | C_integer IChar, _ ->
(if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
else "_si"),
args_uisi e
- | Typing.C_integer (IBool | IUChar | IUInt | IUShort | IULong), _ ->
+ | C_integer (IBool | IUChar | IUInt | IUShort | IULong), _ ->
"_ui", args_uisi e
- | Typing.C_integer (ISChar | IShort | IInt | ILong), _ ->
- "_si", args_uisi e
- | Typing.C_integer (ILongLong | IULongLong as ikind), _ ->
- raise (Longlong ikind)
- | Typing.C_float (FDouble | FFloat), _ ->
- (* FFloat is a strict subset of FDouble (modulo exceptional numbers)
- Hence, calling [set_d] for both of them is sound.
- HOWEVER: the machdep MUST NOT be vulnerable to double rounding
- [TODO] check the statement above *)
- "_d", [ e ]
- | Typing.C_float FLongDouble, _ ->
- Error.not_yet "creating gmp from long double"
- | Typing.Gmpz, _ | Typing.Rational, _ | Typing.Real, _ | Typing.Nan, _ -> (
+ | C_integer (ISChar | IShort | IInt | ILong), _ -> "_si", args_uisi e
+ | C_integer (ILongLong | IULongLong as ikind), _ -> raise (Longlong ikind)
+ | C_float (FDouble | FFloat), _ -> "_d", [ e ]
+ (* FFloat is a strict subset of FDouble (modulo exceptional numbers)
+ Hence, calling [set_d] for both of them is sound.
+ HOWEVER: the machdep MUST NOT be vulnerable to double rounding
+ [TODO] check the statement above *)
+ | C_float FLongDouble, _ -> Error.not_yet "creating gmp from long double"
+ | Gmpz, _ | Rational, _ | Real, _ | Nan, _ -> (
match Cil.unrollType ty with
| TPtr(TInt(IChar, _), _) ->
"_str",
diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index 43f43ce4b77..9738f961d1d 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.ml
+++ b/src/plugins/e-acsl/src/code_generator/libc.ml
@@ -190,7 +190,7 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
let logic_env = Env.Logic_env.get env in
Typing.preprocess_term ~use_gmp_opt:false ~logic_env t;
match Typing.get_number_ty ~logic_env t with
- | Typing.Gmpz ->
+ | Gmpz ->
let e, _, env =
Translate_utils.gmp_to_sizet
~adata:Assert.no_data
@@ -202,7 +202,7 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
t
in
e, env
- | Typing.(C_integer _ | C_float _) as nty ->
+ | C_integer _ | C_float _ as nty ->
(* We know that [t] can be translated to a C type, so we start with that *)
let e, _, env = Translate_terms.to_exp ~adata:Assert.no_data kf env t in
(* Then we can check if the expression will fit in a [size_t] *)
@@ -211,9 +211,8 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
let check_lower_bound, check_upper_bound =
let lower, upper =
match nty with
- | Typing.C_integer t_kind ->
- check_integer_bounds ~from:t_kind sizet_kind
- | Typing.C_float _ -> true, true
+ | C_integer t_kind -> check_integer_bounds ~from:t_kind sizet_kind
+ | C_float _ -> true, true
| _ -> assert false
in
lower && check_lower_bound, upper
@@ -285,9 +284,8 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
List.rev (assigns :: stmts))
in
e, env
- | Typing.(Rational | Real) ->
- Env.not_yet env "cast of rational or real to size_t"
- | Typing.Nan ->
+ | Rational | Real -> Env.not_yet env "cast of rational or real to size_t"
+ | Nan ->
Options.fatal
"Trying to translate a term that is not an integer or a C type: %a"
Printer.pp_term t
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index bd64174a3f0..331ec21a4ea 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -22,6 +22,7 @@
open Cil_types
open Cil_datatype
+open Analyses_types
open Analyses_datatype
module Error = Translation_error
@@ -129,16 +130,16 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
List.fold_right2
(fun lvi pty (params, params_ty) ->
let ty = match pty with
- | Typing.Gmpz ->
+ | Gmpz ->
(* GMP's integer are arrays: consider them as pointers in function's
parameters *)
Gmp_types.Z.t_as_ptr ()
- | Typing.C_integer ik -> TInt(ik, [])
- | Typing.C_float ik -> TFloat(ik, [])
+ | C_integer ik -> TInt(ik, [])
+ | C_float ik -> TFloat(ik, [])
(* for the time being, no reals but rationals instead *)
- | Typing.Rational -> Gmp_types.Q.t ()
- | Typing.Real -> Error.not_yet "real number"
- | Typing.Nan -> Typing.typ_of_lty lvi.lv_type
+ | Rational -> Gmp_types.Q.t ()
+ | Real -> Error.not_yet "real number"
+ | Nan -> Typing.typ_of_lty lvi.lv_type
in
(* build the formals: cannot use [Cil.makeFormal] since the function
does not exist yet *)
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index f7f52b781ff..0f25543b66d 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -309,9 +309,9 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let var_x, x, env = Env.Logic_binding.add ~ty env kf logic_x in
let lv_x = var var_x in
let env = match ctx with
- | Typing.C_integer _ -> env
- | Typing.Gmpz -> Env.add_stmt env (Gmp.init ~loc x)
- | Typing.(C_float _ | Rational | Real | Nan) -> assert false
+ | C_integer _ -> env
+ | Gmpz -> Env.add_stmt env (Gmp.init ~loc x)
+ | C_float _ | Rational | Real | Nan -> assert false
in
(* build the inner loops and loop body *)
let body, env =
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index edfcedde465..db07104aa2d 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -269,7 +269,7 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
Typing.preprocess_term ~use_gmp_opt:false ~logic_env size_term;
let size, adata, env =
match Typing.get_number_ty size_term ~logic_env with
- | Typing.Gmpz ->
+ | Gmpz ->
(* Start by translating [size_term] to an expression so that the full term
with [\let] is not passed around. *)
let size_e, adata, env = !term_to_exp_ref ~adata kf env size_term in
@@ -283,10 +283,8 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
"translation to GMP code should always return a C variable"
in
gmp_to_sizet ~adata ~loc ~pp:size_term kf env cvar_term p
- | Typing.(C_integer _ | C_float _) ->
- !term_to_exp_ref ~adata kf env size_term
- | Typing.(Rational | Real | Nan) ->
- assert false
+ | C_integer _ | C_float _ -> !term_to_exp_ref ~adata kf env size_term
+ | Rational | Real | Nan -> assert false
in
ptr, size, adata, env
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index 718ff8816a1..cf14ab17aa8 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -330,11 +330,11 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
Cil.intType
| PoT_term t ->
begin match Typing.get_number_ty ~logic_env t with
- | Typing.(C_integer _ | C_float _ | Nan) ->
+ | C_integer _ | C_float _ | Nan ->
Typing.get_typ ~logic_env t
- | Typing.(Rational | Real) ->
+ | Rational | Real ->
Error.not_yet "\\at on purely logic variables and over real type"
- | Typing.Gmpz ->
+ | Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
end
in
@@ -357,7 +357,7 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
in
Typing.preprocess_term ~use_gmp_opt:false ~logic_env t_size;
let malloc_stmt = match Typing.get_number_ty ~logic_env t_size with
- | Typing.C_integer IInt ->
+ | C_integer IInt ->
let e_size, _, _ =
term_to_exp ~adata:Assert.no_data kf env t_size
in
@@ -369,11 +369,11 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
[ e_size ]
in
malloc_stmt
- | Typing.(C_integer _ | C_float _ | Gmpz) ->
+ | C_integer _ | C_float _ | Gmpz ->
Error.not_yet
"\\at on purely logic variables that needs to allocate \
too much memory (bigger than int_max bytes)"
- | Typing.(Rational | Real | Nan) ->
+ | Rational | Real | Nan ->
Error.not_yet "quantification over non-integer type"
in
let free_stmt = Smart_stmt.call ~loc "free" [e] in
@@ -411,7 +411,7 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
[ Smart_stmt.block_stmt block ], env
| PoT_term t ->
begin match Typing.get_number_ty ~logic_env t with
- | Typing.(C_integer _ | C_float _ | Nan) ->
+ | C_integer _ | C_float _ | Nan ->
let env = Env.push env in
let lval, env = lval_at_index ~loc kf env (e_at, t_index) in
let e, _, env = term_to_exp kf env t in
@@ -425,9 +425,9 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
[ Smart_stmt.block_stmt block ], env
- | Typing.(Rational | Real) ->
+ | Rational | Real ->
Error.not_yet "\\at on purely logic variables and over real type"
- | Typing.Gmpz ->
+ | Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
end
in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index bfa0d27b5ff..12965127c73 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -55,15 +55,14 @@ let constant_to_exp ~loc env t c =
let logic_env = Env.Logic_env.get env in
let ity = Typing.get_number_ty ~logic_env t in
(match ity with
- | Typing.Nan -> assert false
- | Typing.Real -> Error.not_yet "real number constant"
- | Typing.Rational -> mk_real (Integer.to_string n)
- | Typing.Gmpz ->
- (* too large integer *)
- Cil.mkString ~loc (Integer.to_string n), Typed_number.Str_Z
- | Typing.C_float fkind ->
+ | Nan -> assert false
+ | Real -> Error.not_yet "real number constant"
+ | Rational -> mk_real (Integer.to_string n)
+ | Gmpz -> Cil.mkString ~loc (Integer.to_string n), Typed_number.Str_Z
+ (* too large integer *)
+ | C_float fkind ->
Cil.kfloat ~loc fkind (Int64.to_float (Integer.to_int64_exn n)), C_number
- | Typing.C_integer kind ->
+ | C_integer kind ->
let cast = Typing.get_cast ~logic_env t in
match cast, kind with
| Some ty, (ILongLong | IULongLong) when Gmp_types.Z.is_t ty ->
@@ -716,15 +715,15 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
e, adata, env, Typed_number.C_number, ""
| TBinOp(MinusPP, t1, t2) ->
begin match Typing.get_number_ty ~logic_env t with
- | Typing.C_integer _ ->
+ | C_integer _ ->
let e1, adata, env = to_exp ~adata kf env t1 in
let e2, adata, env = to_exp ~adata kf env t2 in
let ty = Typing.get_typ ~logic_env t in
let e = Cil.new_exp ~loc (BinOp(MinusPP, e1, e2, ty)) in
e, adata, env, Typed_number.C_number, ""
- | Typing.Gmpz ->
+ | Gmpz ->
Env.not_yet env "pointer subtraction resulting in gmp"
- | Typing.(C_float _ | Rational | Real | Nan) ->
+ | C_float _ | Rational | Real | Nan ->
assert false
end
| TCastE(ty, t') ->
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 e66907b425b..5b6f157fc6c 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
@@ -23,6 +23,7 @@
(** Utility functions for generating C implementations. *)
open Cil_types
+open Analyses_types
module Error = Translation_error
(**************************************************************************)
@@ -202,9 +203,9 @@ let comparison_to_exp
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 ->
+ | C_integer _ | C_float _ | Nan ->
Cil.mkBinOp ~loc bop e1 e2, env
- | Typing.Gmpz ->
+ | Gmpz ->
let _, e, env = Env.new_var
~loc
env
@@ -220,10 +221,8 @@ let comparison_to_exp
[ 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"
+ | Rational -> Rational.cmp ~loc bop e1 e2 env kf t_opt
+ | Real -> Error.not_yet "comparison involving real numbers"
end
| _, _ ->
Options.fatal
@@ -283,14 +282,11 @@ let env_of_li ~adata ~loc kf env li =
let vi, vi_e, env = Env.Logic_binding.add ~ty env kf li.l_var_info in
let e, adata, env = !term_to_exp_ref ~adata kf env t in
let stmt = match Typing.get_number_ty ~logic_env t with
- | Typing.(C_integer _ | C_float _ | Nan) ->
+ | C_integer _ | C_float _ | Nan ->
Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
- | Typing.Gmpz ->
- Gmp.init_set ~loc (Cil.var vi) vi_e e
- | Typing.Rational ->
- Rational.init_set ~loc (Cil.var vi) vi_e e
- | Typing.Real ->
- Error.not_yet "real number"
+ | Gmpz -> Gmp.init_set ~loc (Cil.var vi) vi_e e
+ | Rational -> Rational.init_set ~loc (Cil.var vi) vi_e e
+ | Real -> Error.not_yet "real number"
in
adata, Env.add_stmt env stmt
| Ltype _ ->
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.mli b/src/plugins/e-acsl/src/code_generator/translate_utils.mli
index 2932dd4db85..ba8841aa2f4 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.mli
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Analyses_types
(** Utility functions for generating C implementations. *)
@@ -55,7 +56,7 @@ val comparison_to_exp:
loc:location ->
kernel_function ->
Env.t ->
- Typing.number_ty ->
+ number_ty ->
?e1:exp ->
binop ->
term ->
--
GitLab