diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 753d292e132b281ff8d1f041cdb69af1e024343d..61491fcb533b8500099b9d1305c9d414ba69c3ab 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -87,7 +87,7 @@ SRC_CODE_GENERATOR:= \
gmp \
label \
env \
- real \
+ rational \
loops \
quantif \
at_with_lscope \
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 7ed887499ba3ac1622f6727d2cff36319a5d56f6..005b6b8edfd06e12e3997d08616b591453c19557 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -304,7 +304,9 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let vi_of_lv, exp_of_lv, env = Env.Logic_binding.add ~ty env lv in
let e, env = term_to_exp kf env t in
let ty = Cil.typeOf e in
- let init_set = if Real.is_t ty then Real.init_set else Gmp.init_set in
+ let init_set =
+ if Gmp_types.Q.is_t ty then Rational.init_set else Gmp.init_set
+ in
let let_stmt = init_set ~loc (Cil.var vi_of_lv) exp_of_lv e in
let stmts, env =
mk_nested_loops ~loc mk_innermost_block kf env lscope_vars'
@@ -320,9 +322,8 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
Error.not_yet
"creating nested loops from global logic variable"
-
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/code_generator/loops.mli b/src/plugins/e-acsl/src/code_generator/loops.mli
index ed7dd9c48609582174e44991ede2c0b94e2f174a..f2e9fc3fa0fc8a7e7d2c071b7e40d8d4130e000a 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.mli
+++ b/src/plugins/e-acsl/src/code_generator/loops.mli
@@ -70,6 +70,6 @@ val term_to_exp_ref:
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/code_generator/real.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
similarity index 91%
rename from src/plugins/e-acsl/src/code_generator/real.ml
rename to src/plugins/e-acsl/src/code_generator/rational.ml
index 7fb783c32ebb88062d780837043f02d6be0e3f80..815c755da228d1aac5dec3aa3ceaa4455c036268 100644
--- a/src/plugins/e-acsl/src/code_generator/real.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -22,15 +22,6 @@
open Cil_types
-let t () =
- (* When support for irrationals will be provided,
- 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_types.Q.t ()
-
-let is_t ty = Cil_datatype.Typ.equal ty (t ())
-
(* No init_set for GMPQ: init then set separately *)
let init_set ~loc lval vi_e e =
Cil.mkStmt
@@ -39,12 +30,15 @@ let init_set ~loc lval vi_e e =
[ Gmp.init ~loc vi_e ;
Gmp.affect ~loc lval vi_e e ]))
-let mk_real ~loc ?name e env t_opt =
- if Gmp_types.Z.is_t (Cil.typeOf e) then
+let create ~loc ?name e env t_opt =
+ let ty = Cil.typeOf e in
+ if Gmp_types.Z.is_t ty 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 *)
Error.not_yet "reals: creating Q from Z"
+ else if Gmp_types.Q.is_t ty then
+ e, env
else
let _, e, env =
Env.new_var
@@ -52,7 +46,7 @@ let mk_real ~loc ?name e env t_opt =
?name
env
t_opt
- (t ())
+ (Gmp_types.Q.t ())
(fun vi vi_e ->
[ Gmp.init ~loc vi_e ;
Gmp.affect ~loc (Cil.var vi) vi_e e ])
@@ -141,14 +135,14 @@ let normalize_str str =
Error.not_yet "number not written in decimal expansion"
let cast_to_z ~loc:_ ?name:_ e _env =
- assert (is_t (Cil.typeOf e));
+ assert (Gmp_types.Q.is_t (Cil.typeOf e));
Error.not_yet "reals: cast from R to Z"
let add_cast ~loc ?name e env ty =
(* TODO: The best solution would actually be to directly write all the needed
functions as C builtins then just call them here depending on the situation
at hand. *)
- assert (is_t (Cil.typeOf e));
+ assert (Gmp_types.Q.is_t (Cil.typeOf e));
let get_double e env =
let _, e, env =
Env.new_var
@@ -188,14 +182,11 @@ let add_cast ~loc ?name e env ty =
| _ ->
Error.not_yet "R to <typ>"
-let real ~loc e env =
- if is_t (Cil.typeOf e) then e, env else mk_real ~loc e env None
-
let cmp ~loc bop e1 e2 env t_opt =
let fname = "__gmpq_cmp" in
let name = Misc.name_of_binop bop in
- let e1, env = real ~loc e1 env in
- let e2, env = real ~loc e2 env in
+ let e1, env = create ~loc e1 env None (* TODO: t1_opt could be provided *) in
+ let e2, env = create ~loc e2 env None (* TODO: t2_opt could be provided *) in
let _, e, env =
Env.new_var
~loc
@@ -214,7 +205,7 @@ let new_var_and_init ~loc ?scope ?name env t_opt mk_stmts =
?name
env
t_opt
- (t ())
+ (Gmp_types.Q.t ())
(fun v e -> Gmp.init ~loc e :: mk_stmts v e)
let name_arith_bop = function
@@ -227,8 +218,8 @@ let name_arith_bop = function
let binop ~loc bop e1 e2 env t_opt =
let name = name_arith_bop bop in
- let e1, env = real ~loc e1 env in
- let e2, env = real ~loc e2 env in
+ let e1, env = create ~loc e1 env None (* TODO: t1_opt could be provided *) in
+ let e2, env = create ~loc e2 env None (* TODO: t2_opt could be provided *) in
let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
let _, e, env = new_var_and_init ~loc ~name env t_opt mk_stmts in
diff --git a/src/plugins/e-acsl/src/code_generator/real.mli b/src/plugins/e-acsl/src/code_generator/rational.mli
similarity index 83%
rename from src/plugins/e-acsl/src/code_generator/real.mli
rename to src/plugins/e-acsl/src/code_generator/rational.mli
index 1a16c80aa49081803b2070ce6f70cc2713f7242d..94d676097f42f83901223e536da0397196fd883a 100644
--- a/src/plugins/e-acsl/src/code_generator/real.mli
+++ b/src/plugins/e-acsl/src/code_generator/rational.mli
@@ -20,23 +20,11 @@
(* *)
(**************************************************************************)
-(** Realary for real numbers.
- For the sake of maintainability, the only access to the installed
- real library MUST be through the current module.
- For example, if it is `libgmp` then we MUST NEVER directly call gmp
- builtins in outer modules (e.g. `Typing` or `Translate`) for handling reals.
- This way, if we want to change `libgmp` to something else, say `mpfr`, then
- all changes will be centralized here. *)
+(** Generation of rational numbers. *)
open Cil_types
-val t: unit -> typ
-(** C type representing reals in the generated code *)
-
-val is_t: typ -> bool
-(** Is the typ real? *)
-
-val mk_real: loc:location -> ?name:string -> exp -> Env.t -> term option ->
+val create: loc:location -> ?name:string -> exp -> Env.t -> term option ->
exp * Env.t
(** Create a real *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 9779637e2612c47c7fb7c74d95e7e30768ede50f..0c25b00373ac1fef70e3b85f9df6247268bcdaca 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -84,7 +84,7 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
in
let e, env = match strnum with
| Str_Z -> mk_mpz e
- | Str_R -> Real.mk_real ~loc ?name e env t_opt
+ | Str_R -> Rational.create ~loc ?name e env t_opt
| C_number -> e, env
in
match ctx with
@@ -97,9 +97,9 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
(* Z --> Z *)
e, env
| false, true ->
- if Real.is_t ty then
+ if Gmp_types.Q.is_t ty then
(* R --> Z *)
- Real.cast_to_z ~loc ?name e env
+ Rational.cast_to_z ~loc ?name e env
else
(* C integer --> Z *)
let e =
@@ -114,9 +114,9 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
in
mk_mpz e
| _, false ->
- if Real.is_t ctx then
- if Real.is_t (Cil.typeOf e) then (* R --> R *) e, env
- else (* C integer or Z --> R *) Real.mk_real ~loc ?name e env t_opt
+ if Gmp_types.Q.is_t ctx then
+ if Gmp_types.Q.is_t (Cil.typeOf e) then (* R --> R *) e, env
+ else (* C integer or Z --> R *) Rational.create ~loc ?name e env t_opt
else if Gmp_types.Z.is_t ty || strnum = Str_Z then
(* Z --> C type or the integer is represented by a string:
anyway, it fits into a C integer: convert it *)
@@ -134,16 +134,16 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
(fun v _ -> [ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e ] ])
in
e, env
- else if Real.is_t ty || strnum = Str_R then
+ else if Gmp_types.Q.is_t ty || strnum = Str_R then
(* R --> C type or the real is represented by a string *)
- Real.add_cast ~loc ?name e env ctx
+ Rational.add_cast ~loc ?name e env ctx
else
(* C type --> another C type *)
Cil.mkCastT ~force:false ~e ~oldt:ty ~newt:ctx, env
let constant_to_exp ~loc t c =
let mk_real s =
- let s = Real.normalize_str s in
+ let s = Rational.normalize_str s in
Cil.mkString ~loc s, Str_R
in
match c with
@@ -164,7 +164,7 @@ let constant_to_exp ~loc t c =
| Some ty, (ILongLong | IULongLong) when Gmp_types.Z.is_t ty ->
(* too large integer *)
Cil.mkString ~loc (Integer.to_string n), Str_Z
- | Some ty, _ when Real.is_t ty ->
+ | Some ty, _ when Gmp_types.Q.is_t ty ->
mk_real (Integer.to_string n)
| (None | Some _), _ ->
(* do not keep the initial string representation because the generated
@@ -206,7 +206,7 @@ let conditional_to_exp ?(name="if") loc t_opt e1 (e2, env2) (e3, env3) =
let lv = Cil.var v in
let ty = Cil.typeOf ev in
let init_set =
- assert (not (Real.is_t ty));
+ assert (not (Gmp_types.Q.is_t ty));
Gmp.init_set
in
let affect e = init_set ~loc lv ev e in
@@ -299,7 +299,7 @@ and context_insensitive_term_to_exp kf env t =
(fun _ ev -> [ Misc.mk_call ~loc name [ ev; e ] ])
in
e, env, C_number, ""
- else if Real.is_t ty then
+ else if Gmp_types.Q.is_t ty then
not_yet env "reals: Neg | BNot"
else
Cil.new_exp ~loc (UnOp(op, e, ty)), env, C_number, ""
@@ -331,8 +331,8 @@ and context_insensitive_term_to_exp kf env t =
Env.new_var_and_mpz_init ~loc ~name env (Some t) mk_stmts
in
e, env, C_number, ""
- else if Real.is_t ty then
- let e, env = Real.binop ~loc bop e1 e2 env (Some t) in
+ else if Gmp_types.Q.is_t ty then
+ let e, env = Rational.binop ~loc bop e1 e2 env (Some t) in
e, env, C_number, ""
else begin
assert (Logic_typing.is_integral_type t.term_type);
@@ -377,8 +377,8 @@ and context_insensitive_term_to_exp kf env t =
let name = Misc.name_of_binop bop in
let _, e, env = Env.new_var_and_mpz_init ~loc ~name env t mk_stmts in
e, env, C_number, ""
- else if Real.is_t ty then
- let e, env = Real.binop ~loc bop e1 e2 env (Some t) in
+ else if Gmp_types.Q.is_t ty then
+ let e, env = Rational.binop ~loc bop e1 e2 env (Some t) in
e, env, C_number, ""
else begin
assert (Logic_typing.is_integral_type t.term_type);
@@ -611,7 +611,7 @@ and comparison_to_exp
in
Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
| Typing.Rational ->
- Real.cmp ~loc bop e1 e2 env t_opt
+ Rational.cmp ~loc bop e1 e2 env t_opt
| Typing.Real ->
Error.not_yet "comparison involving real numbers"
@@ -642,7 +642,9 @@ and at_to_exp_no_lscope env t_opt label e =
(* either a standard C affectation or a call to an initializer according
to the type of [e] *)
let ty = Cil.typeOf e in
- let init_set = if Real.is_t ty then Real.init_set else Gmp.init_set in
+ let init_set =
+ if Gmp_types.Q.is_t ty then Rational.init_set else Gmp.init_set
+ in
let new_stmt = init_set ~loc (Cil.var res_v) res e in
assert (!env_ref == new_env);
(* generate the new block of code for the labeled statement and the
@@ -672,7 +674,7 @@ and env_of_li li kf env loc =
| Typing.Gmpz ->
Gmp.init_set ~loc (Cil.var vi) vi_e e
| Typing.Rational ->
- Real.init_set ~loc (Cil.var vi) vi_e e
+ Rational.init_set ~loc (Cil.var vi) vi_e e
| Typing.Real ->
Error.not_yet "real number"
in