diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 60896dd441f08ab99346d3f3164da54c353eb714..b637d7e2edc9026f8fd234d12b2b531060683856 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -198,10 +198,10 @@ let acc_list_rev acc l = List.fold_left (fun acc x -> x :: acc) acc l
let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
let local_env, tl_env = top env in
let local_block = local_env.block_info in
- let is_z_t = Gmp.is_z_t ty in
- if is_z_t then Gmp.is_z_now_referenced ();
- let is_q_t = Gmp.is_q_t ty in
- if is_q_t then Gmp.is_q_now_referenced ();
+ let is_z_t = Gmp.Z.is_t ty in
+ if is_z_t then Gmp.Z.is_now_referenced ();
+ let is_q_t = Gmp.Q.is_t ty in
+ if is_q_t then Gmp.Q.is_now_referenced ();
let n = succ env.cpt in
let v =
Cil.makeVarinfo
@@ -301,7 +301,7 @@ let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
?name
env
t
- (Gmp.z_t ())
+ (Gmp.Z.t ())
(fun v e -> Gmp.init ~loc e :: mk_stmts v e)
module Logic_binding = struct
@@ -322,7 +322,7 @@ module Logic_binding = struct
| Some ty -> ty
| None -> match logic_v.lv_type with
| Ctype ty -> ty
- | Linteger -> Gmp.z_t ()
+ | Linteger -> Gmp.Z.t ()
| Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
| Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
let msg =
diff --git a/src/plugins/e-acsl/gmp.ml b/src/plugins/e-acsl/gmp.ml
index 3400dba2492833e104aeb4406eb6aa4705ec86e6..6ebf77419faf23d8261e86aa65a7343d8b107732 100644
--- a/src/plugins/e-acsl/gmp.ml
+++ b/src/plugins/e-acsl/gmp.ml
@@ -23,61 +23,53 @@
open Cil_types
(**************************************************************************)
-(***************************** mpz type ***********************************)
+(***************************** mpz types***********************************)
(**************************************************************************)
-let z_t_torig_ref =
+let mk_dummy_type_info_ref () =
ref
{ torig_name = "";
tname = "";
ttype = TVoid [];
treferenced = false }
-let z_t_struct_torig_ref =
- ref
- { torig_name = "";
- tname = "";
- ttype = TVoid [];
- treferenced = false }
-
-let set_z_t ty = z_t_torig_ref := ty
-
-let is_z_now_referenced () = !z_t_torig_ref.treferenced <- true
-
-let z_t () = TNamed(!z_t_torig_ref, [])
-
-let z_t_ptr () = TNamed(
- {
- torig_name = "";
- tname = "__e_acsl_mpz_struct *";
- ttype = TArray(
- TNamed(!z_t_struct_torig_ref, []),
- Some (Cil.one ~loc:Cil_datatype.Location.unknown),
- {scache = Not_Computed},
- []);
- treferenced = true;
- },
-[])
-
-let is_z_t ty = Cil_datatype.Typ.equal ty (z_t ())
-
-(**************************************************************************)
-(***************************** mpq type ***********************************)
-(**************************************************************************)
-
-let q_t_torig_ref =
- ref
- { torig_name = "";
- tname = "";
- ttype = TVoid [];
- treferenced = false }
-
-let set_q_t ty = q_t_torig_ref := ty
-
-let is_q_now_referenced () = !q_t_torig_ref.treferenced <- true
-
-let q_t () = TNamed(!q_t_torig_ref, [])
-let is_q_t ty = Cil_datatype.Typ.equal ty (q_t ())
+module type S = sig
+ val t: unit -> typ
+ val set_t: typeinfo -> unit
+ val is_now_referenced: unit -> unit
+ val is_t: typ -> bool
+end
+
+module Make(X: sig end) = struct
+ let t_torig_ref = mk_dummy_type_info_ref ()
+ let set_t ty = t_torig_ref := ty
+ let is_now_referenced () = !t_torig_ref.treferenced <- true
+ let t () = TNamed(!t_torig_ref, [])
+ let is_t ty = Cil_datatype.Typ.equal ty (t ())
+end
+
+module Z = struct
+
+ include Make(struct end)
+
+ let t_struct_torig_ref = mk_dummy_type_info_ref ()
+
+ let t_ptr () =
+ TNamed(
+ {
+ torig_name = "";
+ tname = "__e_acsl_mpz_struct *";
+ ttype = TArray(
+ TNamed(!t_struct_torig_ref, []),
+ Some (Cil.one ~loc:Cil_datatype.Location.unknown),
+ {scache = Not_Computed},
+ []);
+ treferenced = true;
+ },
+ [])
+end
+
+module Q = Make(struct end)
(**************************************************************************)
(******************* Initialization of mpz and mpq types ******************)
@@ -89,10 +81,10 @@ let init_t () =
inherit Cil.nopCilVisitor
method !vglob = function
| GType({ torig_name = s } as info, _) when s = "__e_acsl_mpz_t" ->
- set_z_t info;
+ Z.set_t info;
Cil.SkipChildren
| GType({ torig_name = s } as info, _) when s = "__e_acsl_mpq_t" ->
- set_q_t info;
+ Q.set_t info;
Cil.SkipChildren
| _ ->
Cil.SkipChildren
@@ -106,11 +98,12 @@ let init_t () =
let apply_on_var ~loc funname e =
let prefix =
let ty = Cil.typeOf e in
- if is_z_t ty then "__gmpz_"
- else if is_q_t ty then "__gmpq_"
+ if Z.is_t ty then "__gmpz_"
+ else if Q.is_t ty then "__gmpq_"
else assert false
in
Misc.mk_call ~loc (prefix ^ funname) [ e ]
+
let init ~loc e = apply_on_var "init" ~loc e
let clear ~loc e = apply_on_var "clear" ~loc e
@@ -118,7 +111,7 @@ exception Longlong of ikind
let get_set_suffix_and_arg e =
let ty = Cil.typeOf e in
- if is_z_t ty || is_q_t ty then "", [ e ]
+ if Z.is_t ty || Q.is_t ty then "", [ e ]
else
match Cil.unrollType ty with
| TInt(IChar, _) ->
@@ -135,8 +128,9 @@ let get_set_suffix_and_arg e =
[ e; Cil.integer ~loc:e.eloc 10 ]
| TFloat((FDouble | FFloat), _) ->
(* FFloat is a strict subset of FDouble (modulo exceptional numbers)
- Hence, calling [set_d] for bor of them is sound.
- HOWEVER: the machdep MUST NOT be vulnerable to double rounding *)
+ Hence, calling [set_d] for both of them is sound.
+ HOWEVER: the machdep MUST NOT be vulnerable to double rounding *)
+ (* TODO RATIONAL: check machdep *)
"_d", [ e ]
| TFloat(FLongDouble, _) ->
Error.not_yet "creating gmp from long double"
@@ -145,18 +139,19 @@ let get_set_suffix_and_arg e =
let generic_affect ~loc fname lv ev e =
let ty = Cil.typeOf ev in
- if is_z_t ty then begin
+ if Z.is_t ty then begin
assert
- (* Missing cast/wrong typing happened previously *)
- (not (is_q_t (Cil.typeOf e)));
+ (* Missing cast/wrong typing happened in the past *)
+ (not (Q.is_t (Cil.typeOf e)));
let suf, args = get_set_suffix_and_arg e in
Misc.mk_call ~loc (fname ^ suf) (ev :: args)
- end else if is_q_t ty then begin
+ end else if Q.is_t ty then begin
assert
- (* Missing cast/wrong typing happened previously *)
- (not (is_z_t (Cil.typeOf e)));
- (* TODO: If we try to factorize the following the above
- then the result is different... why ?! *)
+ (* Missing cast/wrong typing happened in the past *)
+ (not (Z.is_t (Cil.typeOf e)));
+ (* TODO RATIONAL: [from Fonenantsoa:]
+ If we try to factorize the following the above
+ then the result is different... why ?! *)
let suf, args = get_set_suffix_and_arg e in
Misc.mk_call ~loc (fname ^ suf) (ev :: args)
end else
@@ -165,9 +160,9 @@ let generic_affect ~loc fname lv ev e =
let init_set ~loc lv ev e =
let fname =
let ty = Cil.typeOf ev in
- if is_z_t ty then
+ if Z.is_t ty then
"__gmpz_init_set"
- else if is_q_t ty then
+ else if Q.is_t ty then
Options.fatal "no __gmpq_init_set: init then set separately"
else
""
@@ -177,7 +172,7 @@ let init_set ~loc lv ev e =
| Longlong IULongLong ->
(match e.enode with
| Lval elv ->
- assert (is_z_t (Cil.typeOf ev));
+ assert (Z.is_t (Cil.typeOf ev));
let call = Misc.mk_call
~loc
"__gmpz_import"
@@ -198,8 +193,8 @@ let init_set ~loc lv ev e =
let affect ~loc lv ev e =
let fname =
let ty = Cil.typeOf ev in
- if is_z_t ty then "__gmpz_set"
- else if is_q_t ty then "__gmpq_set"
+ if Z.is_t ty then "__gmpz_set"
+ else if Q.is_t ty then "__gmpq_set"
else ""
in
try generic_affect ~loc fname lv ev e
diff --git a/src/plugins/e-acsl/gmp.mli b/src/plugins/e-acsl/gmp.mli
index f115edd1ad6c24684e37735b68f55d4109f2b71d..78431aeecfd727b9620f6b184f0824568f0fb2e5 100644
--- a/src/plugins/e-acsl/gmp.mli
+++ b/src/plugins/e-acsl/gmp.mli
@@ -24,35 +24,29 @@
open Cil_types
-(**************************************************************************)
-(******************************** Types ***********************************)
-(**************************************************************************)
-
val init_t: unit -> unit
(** Must be called before any use of GMP *)
-val set_z_t: typeinfo -> unit
-val set_q_t: typeinfo -> unit
-
-val z_t: unit -> typ
-(** type [mpz_t] *)
+(**************************************************************************)
+(******************************** Types ***********************************)
+(**************************************************************************)
-val z_t_ptr: unit -> typ
+module type S = sig
+ val t: unit -> typ
+ val set_t: typeinfo -> unit
+ val is_now_referenced: unit -> unit
+ val is_t: typ -> bool
+end
+
+(** Representation of the unbounded integer type at runtime *)
+module Z: sig
+ include S
+ val t_ptr: unit -> typ
(** type "_mpz_struct *" *)
+end
-val q_t: unit -> typ
-(** type [mpq_t] *)
-
-val is_z_now_referenced: unit -> unit
-(** Should be called once one variable of type [mpz_t] exists *)
-
-val is_q_now_referenced: unit -> unit
-(** Should be called once one variable of type [mpq_t] exists *)
-
-val is_z_t: typ -> bool
-(** is the type equal to [mpz_t]? *)
-val is_q_t: typ -> bool
-(** is the type equal to [mpq_t]? *)
+(** Representation of the rational type at runtime *)
+module Q: S
(**************************************************************************)
(************************* Calls to builtins ******************************)
diff --git a/src/plugins/e-acsl/logic_functions.ml b/src/plugins/e-acsl/logic_functions.ml
index 5c8fae25984e9aa118d5bbcb914acdeaa35b126d..f9b4a47a05ecd427340f3f866e90c02df3179261 100644
--- a/src/plugins/e-acsl/logic_functions.ml
+++ b/src/plugins/e-acsl/logic_functions.ml
@@ -41,7 +41,7 @@ let term_to_exp_ref
(* @return true iff the result of the function is provided by reference as the
first extra argument at each call *)
-let result_as_extra_argument = Gmp.is_z_t
+let result_as_extra_argument = Gmp.Z.is_t
(* TODO: to be extended to any compound type? E.g. returning a struct is not
good practice... *)
@@ -125,7 +125,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
| Typing.Gmpz ->
(* GMP's integer are arrays: consider them as pointers in function's
parameters *)
- Gmp.z_t_ptr ()
+ Gmp.Z.t_ptr ()
| Typing.C_type ik -> TInt(ik, [])
| Typing.Real ->
(* TODO RATIONAL: implement this case *)
@@ -196,7 +196,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
| TInt _ as ty -> Interval.Env.add lvi (Interval.interv_of_typ ty)
| ty ->
(* TODO RATIONAL: what to do with rationals? *)
- if Gmp.is_z_t ty then
+ if Gmp.Z.is_t ty then
Interval.Env.add lvi (Ival.inject_range None None));
Env.Logic_binding.add_binding env lvi vi
in
diff --git a/src/plugins/e-acsl/real.ml b/src/plugins/e-acsl/real.ml
index cc605e94b44842554d984fc59e79ea79db67cbfb..964f5913c0e111177eda0e084b8efff5da35e55a 100644
--- a/src/plugins/e-acsl/real.ml
+++ b/src/plugins/e-acsl/real.ml
@@ -27,7 +27,7 @@ let t () =
the following typ MUST be changed into a typ that can represent them.
It is sound to use GMPQ for the time being since irrationals
raise not_yet. *)
- Gmp.q_t ()
+ Gmp.Q.t ()
let is_t ty = Cil_datatype.Typ.equal ty (t ())
@@ -40,7 +40,7 @@ let init_set ~loc lval vi_e e =
Gmp.affect ~loc lval vi_e e ]))
let mk_real ~loc ?name e env t_opt =
- if Gmp.is_z_t (Cil.typeOf e) then
+ if Gmp.Z.is_t (Cil.typeOf e) then
(* GMPQ has no builtin for creating Q from Z. Hence:
1) Get the MPZ as a string: gmZ_get_str
2) Set the MPQ with that string: gmpQ_set_str *)
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index d272f044e7d31d5d867a7cd90a1d597c08bb40b4..9c1e04a02c8264199e3252eb2b1e3668489a3046 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -73,7 +73,7 @@ let add_cast ~loc ?name env ctx sty t_opt e =
?name
env
t_opt
- (Gmp.z_t ())
+ (Gmp.Z.t ())
(fun lv v -> [ Gmp.init_set ~loc (Cil.var lv) v e ])
in
e, env
@@ -88,8 +88,8 @@ let add_cast ~loc ?name env ctx sty t_opt e =
e, env
| Some ctx ->
let ty = Cil.typeOf e in
- if Gmp.is_z_t ctx then
- if Gmp.is_z_t ty then
+ if Gmp.Z.is_t ctx then
+ if Gmp.Z.is_t ty then
e, env
else if Real.is_t ty then
Real.cast_to_z ~loc ?name e env
@@ -113,7 +113,7 @@ let add_cast ~loc ?name env ctx sty t_opt e =
else Real.mk_real ~loc ?name e env t_opt
else
(* handle a C-integer context *)
- if Gmp.is_z_t ty || sty = StrZ then
+ if Gmp.Z.is_t ty || sty = StrZ then
(* we get an mpz, but it fits into a C integer: convert it *)
let fname, new_ty =
if Cil.isSignedInteger ctx then
@@ -155,7 +155,7 @@ let constant_to_exp ~loc t c =
| Typing.C_type kind ->
let cast = Typing.get_cast t in
match cast, kind with
- | Some ty, (ILongLong | IULongLong) when Gmp.is_z_t ty ->
+ | Some ty, (ILongLong | IULongLong) when Gmp.Z.is_t ty ->
raise Cil.Not_representable
| Some ty, (ILongLong | IULongLong) when Real.is_t ty ->
mk_real (Integer.to_string n)
@@ -273,7 +273,7 @@ and context_insensitive_term_to_exp kf env t =
| TUnOp(Neg | BNot as op, t') ->
let ty = Typing.get_typ t in
let e, env = term_to_exp kf env t' in
- if Gmp.is_z_t ty then
+ if Gmp.Z.is_t ty then
let name, vname = match op with
| Neg -> "__gmpz_neg", "neg"
| BNot -> "__gmpz_com", "bnot"
@@ -294,7 +294,7 @@ and context_insensitive_term_to_exp kf env t =
Cil.new_exp ~loc (UnOp(op, e, ty)), env, Not_a_strnum, ""
| TUnOp(LNot, t) ->
let ty = Typing.get_op t in
- if Gmp.is_z_t ty then
+ if Gmp.Z.is_t ty then
(* [!t] is converted into [t == 0] *)
let zero = Logic_const.tinteger 0 in
let ctx = Typing.get_number_ty t in
@@ -314,7 +314,7 @@ and context_insensitive_term_to_exp kf env t =
let ty = Typing.get_typ t in
let e1, env = term_to_exp kf env t1 in
let e2, env = term_to_exp kf env t2 in
- if Gmp.is_z_t ty then
+ if Gmp.Z.is_t ty then
let name = name_of_mpz_arith_bop bop in
let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
@@ -334,7 +334,7 @@ and context_insensitive_term_to_exp kf env t =
let ty = Typing.get_typ t in
let e1, env = term_to_exp kf env t1 in
let e2, env = term_to_exp kf env t2 in
- if Gmp.is_z_t ty then
+ if Gmp.Z.is_t ty then
(* TODO: preventing division by zero should not be required anymore.
RTE should do this automatically. *)
let ctx = Typing.get_number_ty t in
@@ -352,7 +352,7 @@ and context_insensitive_term_to_exp kf env t =
~loc kf env Typing.gmpz ~e1:e2 ~name Eq t2 zero t
in
let mk_stmts _v e =
- assert (Gmp.is_z_t ty);
+ assert (Gmp.Z.is_t ty);
let vis = Env.get_visitor env in
let kf = Extlib.the vis#current_kf in
let cond =
@@ -904,7 +904,7 @@ exception No_simple_translation of term
let term_to_exp typ t =
(* infer a context from the given [typ] whenever possible *)
let ctx_of_typ ty =
- if Gmp.is_z_t ty then Typing.gmpz
+ if Gmp.Z.is_t ty then Typing.gmpz
else if Real.is_t ty then Typing.libr
else
match ty with
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 19a4c29321d09e19fe658f4c2aaeacc6c6536d00..8b07afe76a02ac7ed8cb2d4d5cf76633f1c0f02f 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -107,13 +107,13 @@ let join ty1 ty2 = match ty1, ty2 with
exception Not_a_number
let typ_of_number_ty = function
| C_type ik -> TInt(ik, [])
- | Gmpz -> Gmp.z_t ()
+ | Gmpz -> Gmp.Z.t ()
| Real -> Real.t ()
| Nan -> raise Not_a_number
let typ_of_lty = function
| Ctype cty -> cty
- | Linteger -> Gmp.z_t ()
+ | Linteger -> Gmp.Z.t ()
| Lreal ->
(* TODO RATIONAL: implement this case *)
assert false