From 0324062d1c0c5dbd9f68b8ebd611cdeb23809f3b Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 2 Aug 2019 17:08:53 +0200
Subject: [PATCH] [rational] rename Libr to Real
---
src/plugins/e-acsl/Makefile.in | 2 +-
src/plugins/e-acsl/at_with_lscope.ml | 6 +--
src/plugins/e-acsl/functions.mli | 2 +-
src/plugins/e-acsl/interval.ml | 2 +-
src/plugins/e-acsl/interval.mli | 2 +-
src/plugins/e-acsl/logic_functions.ml | 2 +-
src/plugins/e-acsl/loops.ml | 4 +-
src/plugins/e-acsl/mmodel_translate.ml | 2 +-
src/plugins/e-acsl/{libr.ml => real.ml} | 0
src/plugins/e-acsl/{libr.mli => real.mli} | 2 +-
src/plugins/e-acsl/temporal.ml | 2 +-
src/plugins/e-acsl/translate.ml | 50 +++++++++++------------
src/plugins/e-acsl/typing.ml | 34 +++++++--------
src/plugins/e-acsl/typing.mli | 4 +-
14 files changed, 57 insertions(+), 57 deletions(-)
rename src/plugins/e-acsl/{libr.ml => real.ml} (100%)
rename src/plugins/e-acsl/{libr.mli => real.mli} (99%)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 43c869e1d62..d47d30b3a59 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 759e9473bf3..381dfaa5a83 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 c549f3abc4c..4c1c01fefda 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 8124f877b46..4be4936970d 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 e28ffe653a6..e041ef8e7d3 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 f7f83847db7..5c8fae25984 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 4d44b77ef1e..c9b0f712858 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 8fc258a765b..7457de1d8cd 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 93663f8cf2e..cca50791d97 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 d624f2ebd57..e7bf4e97376 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 e184862b1db..d272f044e7d 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 9caa4380d37..19a4c29321d 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 1c674dca7fd..38dba48cbd2 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
--
GitLab