diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 43c869e1d62348f588578b3e8e85c10d3427bd08..d47d30b3a59c1c6f3c28e8a33b81a09ee490b017 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -71,7 +71,7 @@ PLUGIN_CMO:= local_config \
label \
lscope \
env \
- libr \
+ real \
keep_status \
dup_functions \
interval \
diff --git a/src/plugins/e-acsl/at_with_lscope.ml b/src/plugins/e-acsl/at_with_lscope.ml
index 759e9473bf3c212035871a22408c5556436d1f77..381dfaa5a83bbfe253dd0a2060e9c1827f7ca3fc 100644
--- a/src/plugins/e-acsl/at_with_lscope.ml
+++ b/src/plugins/e-acsl/at_with_lscope.ml
@@ -232,7 +232,7 @@ let to_exp ~loc kf env pot label =
begin match Typing.get_number_ty t with
| Typing.C_type _ | Typing.Nan ->
Typing.get_typ t
- | Typing.Libr ->
+ | Typing.Real ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
@@ -267,7 +267,7 @@ let to_exp ~loc kf env pot label =
Error.not_yet
"\\at on purely logic variables that needs to allocate \
too much memory (bigger than int_max bytes)"
- | Typing.Libr | Typing.Nan ->
+ | Typing.Real | Typing.Nan ->
Options.fatal
"quantification over non-integer type is not part of E-ACSL"
in
@@ -317,7 +317,7 @@ let to_exp ~loc kf env pot label =
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
[ Cil.mkStmt ~valid_sid:true (Block block) ], env
- | Typing.Libr ->
+ | Typing.Real ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
diff --git a/src/plugins/e-acsl/functions.mli b/src/plugins/e-acsl/functions.mli
index c549f3abc4c59ac67bc7eb7a1dc4351ee54b74e3..4c1c01fefdaa5b47c9ec3b0ef6a2e7b49353fbf7 100644
--- a/src/plugins/e-acsl/functions.mli
+++ b/src/plugins/e-acsl/functions.mli
@@ -61,7 +61,7 @@ module RTL: sig
val is_rtl_name: string -> bool
(** @return [true] if the prefix of the given name indicates that it
- belongs to the public API of the E-ACSL Runtime Library *)
+ belongs to the public API of the E-ACSL Runtime Realary *)
val is_generated_literal_string_name: string -> bool
(** Same as [is_generated_name] but indicates that the name represents a local
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 8124f877b464b77202abecfbe71aab6c897ef989..4be4936970dd126c51fb33454bcd22cebe7efaf5 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -62,7 +62,7 @@ let rec interv_of_typ_with_real ty is_real = match Cil.unrollType ty with
| TFloat _ ->
(* TODO: Do not systematically consider floats as reals for efficiency *)
Ival.bottom, true
- | _ when Libr.is_t ty ->
+ | _ when Real.is_t ty ->
Ival.bottom, true
| _ ->
raise Not_a_number
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index e28ffe653a6f75c953eef51d7772827818fcd301..e041ef8e7d32ca005cd63b9c42332b54e82085de 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -62,7 +62,7 @@ val ikind_of_interv: Ival.t -> Cil_types.ikind
val interv_of_typ: Cil_types.typ -> Ival.t
(** @return the smallest interval which contains the given C type.
@raise Is_a_real if the given type is a float type.
- (* TODO: also return is_real=true if ty=Libr.t *)
+ (* TODO: also return is_real=true if ty=Real.t *)
@raise Not_a_number if the given type does not represent numbers. *)
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/logic_functions.ml b/src/plugins/e-acsl/logic_functions.ml
index f7f83847db72d0406bec9cbf5e403cccbfe0286f..5c8fae25984e9aa118d5bbcb914acdeaa35b126d 100644
--- a/src/plugins/e-acsl/logic_functions.ml
+++ b/src/plugins/e-acsl/logic_functions.ml
@@ -127,7 +127,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
parameters *)
Gmp.z_t_ptr ()
| Typing.C_type ik -> TInt(ik, [])
- | Typing.Libr ->
+ | Typing.Real ->
(* TODO RATIONAL: implement this case *)
assert false
| Typing.Nan -> Typing.typ_of_lty lvi.lv_type
diff --git a/src/plugins/e-acsl/loops.ml b/src/plugins/e-acsl/loops.ml
index 4d44b77ef1ec035f591392d86fb17ba70277aa62..c9b0f71285883a773dc0aececd706c02d90c55c3 100644
--- a/src/plugins/e-acsl/loops.ml
+++ b/src/plugins/e-acsl/loops.ml
@@ -224,7 +224,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let env = match ctx_one with
| Typing.C_type _ -> env
| Typing.Gmpz -> Env.add_stmt env (Gmp.init ~loc x)
- | Typing.Libr | Typing.Nan -> assert false
+ | Typing.Real | Typing.Nan -> assert false
in
(* build the inner loops and loop body *)
let body, env =
@@ -304,7 +304,7 @@ 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 Libr.is_t ty then Libr.init_set else Gmp.init_set in
+ let init_set = if Real.is_t ty then Real.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'
diff --git a/src/plugins/e-acsl/mmodel_translate.ml b/src/plugins/e-acsl/mmodel_translate.ml
index 8fc258a765b821a1439e349e8c98b16b620813cd..7457de1d8cda7bc72736ca81a586c1795fb9a226 100644
--- a/src/plugins/e-acsl/mmodel_translate.ml
+++ b/src/plugins/e-acsl/mmodel_translate.ml
@@ -214,7 +214,7 @@ let call_memory_block ~loc kf name ctx env ptr r p =
| Typing.C_type _ ->
let size, env = term_to_exp kf env size_term in
Cil.constFold false size, env
- | Typing.Libr | Typing.Nan ->
+ | Typing.Real | Typing.Nan ->
assert false
in
(* base and base_addr *)
diff --git a/src/plugins/e-acsl/libr.ml b/src/plugins/e-acsl/real.ml
similarity index 100%
rename from src/plugins/e-acsl/libr.ml
rename to src/plugins/e-acsl/real.ml
diff --git a/src/plugins/e-acsl/libr.mli b/src/plugins/e-acsl/real.mli
similarity index 99%
rename from src/plugins/e-acsl/libr.mli
rename to src/plugins/e-acsl/real.mli
index 93663f8cf2e0ecef11207428db3839ca0983d707..cca50791d978c1b19f55248c5de54a8e31c29ec9 100644
--- a/src/plugins/e-acsl/libr.mli
+++ b/src/plugins/e-acsl/real.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(** Library for real numbers.
+(** 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
diff --git a/src/plugins/e-acsl/temporal.ml b/src/plugins/e-acsl/temporal.ml
index d624f2ebd5759775f0ffba685a311267ac90a572..e7bf4e973761b80fdabd9f309cc9f8761ef36771 100644
--- a/src/plugins/e-acsl/temporal.ml
+++ b/src/plugins/e-acsl/temporal.ml
@@ -284,7 +284,7 @@ end = struct
let rhs = Cil.new_exp ~loc (Lval ret) in
let vals = assign ret rhs loc in
(* Track referent numbers of assignments via function calls.
- Library functions (i.e., with no source code available) that return
+ Realary functions (i.e., with no source code available) that return
values are considered to be functions that allocate memory. They are
considered so because they need to be handled exactly as memory
allocating functions, that is, the referent of the returned pointer is
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index e184862b1db116f7671cc01ac3a3897fdcc75dbd..d272f044e7d31d5d867a7cd90a1d597c08bb40b4 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -80,7 +80,7 @@ let add_cast ~loc ?name env ctx sty t_opt e =
in
let e, env = match sty with
| StrZ -> mk_mpz e
- | StrR -> Libr.mk_real ~loc ?name e env t_opt
+ | StrR -> Real.mk_real ~loc ?name e env t_opt
| Not_a_strnum -> e, env
in
match ctx with
@@ -91,8 +91,8 @@ let add_cast ~loc ?name env ctx sty t_opt e =
if Gmp.is_z_t ctx then
if Gmp.is_z_t ty then
e, env
- else if Libr.is_t ty then
- Libr.cast_to_z ~loc ?name e env
+ else if Real.is_t ty then
+ Real.cast_to_z ~loc ?name e env
else
(* Convert the C integer into a mpz.
Remember: very long integer constants have been temporary converted
@@ -108,9 +108,9 @@ let add_cast ~loc ?name env ctx sty t_opt e =
assert false
in
mk_mpz e
- else if Libr.is_t ctx then
- if Libr.is_t (Cil.typeOf e) then e, env
- else Libr.mk_real ~loc ?name e env t_opt
+ else if Real.is_t ctx then
+ if Real.is_t (Cil.typeOf e) then e, env
+ 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
@@ -131,14 +131,14 @@ let add_cast ~loc ?name env ctx sty t_opt e =
(fun v _ -> [ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e ] ])
in
e, env
- else if Libr.is_t ty || sty = StrR then
- Libr.add_cast ~loc ?name e env ctx
+ else if Real.is_t ty || sty = StrR then
+ Real.add_cast ~loc ?name e env ctx
else
Cil.mkCastT ~force:false ~e ~oldt:ty ~newt:ctx, env
let constant_to_exp ~loc t c =
let mk_real s =
- let s = Libr.normalize_str s in
+ let s = Real.normalize_str s in
Cil.mkString ~loc s, StrR
in
match c with
@@ -148,7 +148,7 @@ let constant_to_exp ~loc t c =
match ity with
| Typing.Nan ->
assert false
- | Typing.Libr ->
+ | Typing.Real ->
mk_real (Integer.to_string n)
| Typing.Gmpz ->
raise Cil.Not_representable
@@ -157,7 +157,7 @@ let constant_to_exp ~loc t c =
match cast, kind with
| Some ty, (ILongLong | IULongLong) when Gmp.is_z_t ty ->
raise Cil.Not_representable
- | Some ty, (ILongLong | IULongLong) when Libr.is_t ty ->
+ | Some ty, (ILongLong | IULongLong) when Real.is_t ty ->
mk_real (Integer.to_string n)
| (None | Some _), _ ->
(* do not keep the initial string representation because the
@@ -200,7 +200,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 =
- if Libr.is_t ty then Libr.init_set else Gmp.init_set
+ if Real.is_t ty then Real.init_set else Gmp.init_set
in
let affect e = init_set ~loc lv ev e in
let then_block, _ =
@@ -288,7 +288,7 @@ and context_insensitive_term_to_exp kf env t =
(fun _ ev -> [ Misc.mk_call ~loc name [ ev; e ] ])
in
e, env, Not_a_strnum, ""
- else if Libr.is_t ty then
+ else if Real.is_t ty then
not_yet env "reals: Neg | BNot"
else
Cil.new_exp ~loc (UnOp(op, e, ty)), env, Not_a_strnum, ""
@@ -303,7 +303,7 @@ and context_insensitive_term_to_exp kf env t =
kf ~loc ~name:"not" env Typing.gmpz Eq t zero (Some t)
in
e, env, Not_a_strnum, ""
- else if Libr.is_t ty then
+ else if Real.is_t ty then
not_yet env "reals: LNot"
else begin
assert (Cil.isIntegralType ty);
@@ -322,8 +322,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, Not_a_strnum, ""
- else if Libr.is_t ty then
- let e, env = Libr.binop ~loc bop e1 e2 env (Some t) in
+ else if Real.is_t ty then
+ let e, env = Real.binop ~loc bop e1 e2 env (Some t) in
e, env, Not_a_strnum, ""
else
if Logic_typing.is_integral_type t.term_type then
@@ -369,8 +369,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, Not_a_strnum, ""
- else if Libr.is_t ty then
- let e, env = Libr.binop ~loc bop e1 e2 env (Some t) in
+ else if Real.is_t ty then
+ let e, env = Real.binop ~loc bop e1 e2 env (Some t) in
e, env, Not_a_strnum, ""
else
(* no guard required since RTEs are generated separately *)
@@ -430,7 +430,7 @@ and context_insensitive_term_to_exp kf env t =
Cil.new_exp ~loc (BinOp(MinusPP, e1, e2, ty)), env, Not_a_strnum, ""
| Typing.Gmpz ->
not_yet env "pointer subtraction resulting in gmp"
- | Typing.Libr | Typing.Nan ->
+ | Typing.Real | Typing.Nan ->
assert false
end
| TCastE(ty, t') ->
@@ -604,8 +604,8 @@ and comparison_to_exp
[ Misc.mk_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.Libr ->
- Libr.cmp ~loc bop e1 e2 env t_opt
+ | Typing.Real ->
+ Real.cmp ~loc bop e1 e2 env t_opt
and at_to_exp_no_lscope env t_opt label e =
let stmt = E_acsl_label.get_stmt (Env.get_visitor env) label in
@@ -634,7 +634,7 @@ and at_to_exp_no_lscope env t_opt label e =
(* either a standard C affectation or something else according to type of
[e] *)
let ty = Cil.typeOf e in
- let init_set = if Libr.is_t ty then Libr.init_set else Gmp.init_set in
+ let init_set = if Real.is_t ty then Real.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
@@ -663,8 +663,8 @@ and env_of_li li kf env loc =
Cil.mkStmtOneInstr (Set (Cil.var vi, e, loc))
| Typing.Gmpz ->
Gmp.init_set ~loc (Cil.var vi) vi_e e
- | Typing.Libr ->
- Libr.init_set ~loc (Cil.var vi) vi_e e
+ | Typing.Real ->
+ Real.init_set ~loc (Cil.var vi) vi_e e
in
Env.add_stmt env stmt
@@ -905,7 +905,7 @@ 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
- else if Libr.is_t ty then Typing.libr
+ else if Real.is_t ty then Typing.libr
else
match ty with
| TInt(ik, _) -> Typing.ikind ik
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 9caa4380d3791c702f699065dda594e707d0c5f0..19a4c29321d09e19fe658f4c2aaeacc6c6536d00 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -39,13 +39,13 @@ let compute_quantif_guards_ref
type number_ty =
| C_type of ikind
| Gmpz
- | Libr
+ | Real
| Nan
let c_int = C_type IInt
let ikind ik = C_type ik
let gmpz = Gmpz
-let libr = Libr
+let libr = Real
let nan = Nan
module D =
@@ -86,11 +86,11 @@ module D =
let join ty1 ty2 = match ty1, ty2 with
| Nan, Nan ->
Nan
- | Nan, Libr | Libr, Nan ->
+ | Nan, Real | Real, Nan ->
Options.fatal "[typing] join failure: real and nan"
- | Libr, Libr -> Libr
- | Libr, (Gmpz | C_type _) | (Gmpz | C_type _), Libr ->
- Libr
+ | Real, Real -> Real
+ | Real, (Gmpz | C_type _) | (Gmpz | C_type _), Real ->
+ Real
| Nan, (Gmpz | C_type _) | (Gmpz | C_type _), Nan ->
Options.fatal "[typing] join failure: integer and nan"
| Gmpz, _ | _, Gmpz -> Gmpz
@@ -108,7 +108,7 @@ exception Not_a_number
let typ_of_number_ty = function
| C_type ik -> TInt(ik, [])
| Gmpz -> Gmp.z_t ()
- | Libr -> Libr.t ()
+ | Real -> Real.t ()
| Nan -> raise Not_a_number
let typ_of_lty = function
@@ -185,9 +185,9 @@ let ty_of_logic_ty = function
| Linteger -> Gmpz
| Ctype ty -> (match Cil.unrollType ty with
| TInt(ik, _) -> C_type ik
- | TFloat _ -> Libr
+ | TFloat _ -> Real
| _ -> Nan)
- | Lreal -> Libr
+ | Lreal -> Real
| Larrow _ -> Nan
| Ltype _ -> Error.not_yet "user-defined logic type"
| Lvar _ -> Error.not_yet "type variable"
@@ -205,10 +205,10 @@ let ty_of_interv ?ctx i =
| None | Some (Gmpz | Nan) -> C_type kind
| Some (C_type ik as ctx) ->
if Cil.intTypeIncluded kind ik then ctx else C_type kind
- | Some Libr -> Libr)
+ | Some Real -> Real)
with Cil.Not_representable ->
match ctx with
- | Some (Libr) -> Libr
+ | Some (Real) -> Real
| None | Some _ -> Gmpz
(* compute a new {!computed_info} by coercing the given type [ty] to the given
@@ -250,7 +250,7 @@ let offset_ty t =
is true. *)
let mk_ctx ~use_gmp_opt = function
| C_type _ as c -> if use_gmp_opt && Options.Gmp_only.get () then Gmpz else c
- | Gmpz | Libr | Nan as c -> c
+ | Gmpz | Real | Nan as c -> c
let infer_if_integer li =
let li_t = Misc.term_of_li li in
@@ -258,7 +258,7 @@ let infer_if_integer li =
| C_type _ | Gmpz ->
let i = Interval.infer li_t in
Interval.Env.add li.l_var_info i
- | Libr | Nan ->
+ | Real | Nan ->
()
(* type the term [t] in a context [ctx] by taking --e-acsl-gmp-only into account
@@ -402,7 +402,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
ignore (type_term ~use_gmp_opt:true ~ctx t2);
let ty = match ctx with
| Nan -> c_int
- | Libr | Gmpz | C_type _ -> ctx
+ | Real | Gmpz | C_type _ -> ctx
in
c_int, ty
@@ -623,7 +623,7 @@ let rec type_predicate p =
ignore (type_term ~use_gmp_opt:true ~ctx t2);
(match ctx with
| Nan -> c_int
- | Libr | Gmpz | C_type _ -> ctx)
+ | Real | Gmpz | C_type _ -> ctx)
| Pand(p1, p2)
| Por(p1, p2)
| Pxor(p1, p2)
@@ -691,7 +691,7 @@ let rec type_predicate p =
| C_type _ -> i
| Gmpz -> Ival.inject_range None None (* [ -\infty; +\infty ] *)
| Nan -> assert false
- | Libr -> Error.not_yet "reals: quantification"
+ | Real -> Error.not_yet "reals: quantification"
in
Interval.Env.add x i)
guards;
@@ -749,7 +749,7 @@ let extract_typ t ty =
| Ctype _ ->
Logic_utils.logicCType lty
| Lreal ->
- Libr.t ()
+ Real.t ()
| Ltype _ | Lvar _ | Linteger | Larrow _ ->
if Cil.isLogicRealType lty then TFloat(FLongDouble, [])
else if Cil.isLogicFloatType lty then Logic_utils.logicCType lty
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 1c674dca7fd5d88c0d38749ff9eabd0402c38f68..38dba48cbd257eaee239bede00fcb019f97fa272 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -55,7 +55,7 @@ open Cil_types
type number_ty = private
| C_type of ikind
| Gmpz
- | Libr
+ | Real
| Nan
module Datatype: Datatype.S_with_collections with type t = number_ty
@@ -73,7 +73,7 @@ val nan: number_ty
exception Not_a_number
val typ_of_number_ty: number_ty -> typ
(** @return the C type corresponding to an {!number_ty}. That is [Gmp.z_t ()]
- for [Gmpz], [Libr.t ()] for [Libr] and [TInt(ik, [[]])] for [Ctype ik].
+ for [Gmpz], [Real.t ()] for [Real] and [TInt(ik, [[]])] for [Ctype ik].
@raise Not_a_number in case of [Nan]. *)
val number_ty_of_typ: typ -> number_ty