Commit 0324062d authored by Julien Signoles's avatar Julien Signoles
Browse files

[rational] rename Libr to Real

parent 11b9381a
......@@ -71,7 +71,7 @@ PLUGIN_CMO:= local_config \
label \
lscope \
env \
libr \
real \
keep_status \
dup_functions \
interval \
......
......@@ -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"
......
......@@ -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
......
......@@ -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
......
......@@ -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. *)
(* ************************************************************************** *)
......
......@@ -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
......
......@@ -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'
......
......@@ -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 *)
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment