From d64d60138c258dd1527df682314d349ac4a81c1a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 31 Mar 2020 10:59:30 +0200
Subject: [PATCH] [kernel] renaming & typos in logic utils
---
src/kernel_services/ast_data/alarms.ml | 8 +++----
.../ast_queries/logic_utils.ml | 22 +++++++++----------
.../ast_queries/logic_utils.mli | 12 +++++-----
3 files changed, 21 insertions(+), 21 deletions(-)
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 903e79bb9f0..a0845e81504 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -452,13 +452,13 @@ let overflowed_expr_to_term ~loc e =
match e.enode with
| UnOp(op, e, ty) ->
let t = Logic_utils.expr_to_term ~coerce:true e in
- let ty = Logic_utils.coerced ty in
- Logic_const.term ~loc (TUnOp(op, t)) ty
+ let lty = Logic_utils.coerce_type ty in
+ Logic_const.term ~loc (TUnOp(op, t)) lty
| BinOp(op, e1, e2, ty) ->
let t1 = Logic_utils.expr_to_term ~coerce:true e1 in
let t2 = Logic_utils.expr_to_term ~coerce:true e2 in
- let ty = Logic_utils.coerced ty in
- Logic_const.term ~loc (TBinOp(op, t1, t2)) ty
+ let lty = Logic_utils.coerce_type ty in
+ Logic_const.term ~loc (TBinOp(op, t1, t2)) lty
| _ -> Logic_utils.expr_to_term ~coerce:true e
(* Creates \is_finite((fkind)e) or \is_nan((fkind)e) according to
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index b3fa33f9651..18313884188 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -123,7 +123,7 @@ let plain_array_to_ptr ty =
let array_to_ptr = plain_or_set plain_array_to_ptr
-let coerced typ =
+let coerce_type typ =
let ty = Cil.unrollType typ in
if Cil.isIntegralType ty then Linteger
else if Cil.isFloatingType ty then Lreal
@@ -341,7 +341,7 @@ let is_zero_comparable t =
let scalar_term_conversion conversion t =
let loc = t.term_loc in
- let arith_conversion t =
+ let int_conversion t =
conversion ~loc false t (Cil.lzero ~loc ()) in
let real_conversion ?ltyp t =
conversion ~loc false t (Logic_const.treal_zero ~loc ?ltyp ()) in
@@ -351,14 +351,14 @@ let scalar_term_conversion conversion t =
let ctrue = Logic_env.Logic_ctor_info.find "\\true" in
conversion ~loc true t (term ~loc (TDataCons(ctrue,[])) boolean_type) in
match unroll_type t.term_type with
- | Ctype (TInt _) -> arith_conversion t
+ | Ctype (TInt _) -> int_conversion t
| Ctype (TFloat _) as ltyp -> real_conversion ~ltyp t
| Ctype (TPtr _) -> ptr_conversion t
| Ctype (TArray _) -> ptr_conversion t
(* Could be transformed to \true: an array is never \null *)
| Ctype (TFun _) -> ptr_conversion t
(* decay as pointer *)
- | Linteger -> arith_conversion t
+ | Linteger -> int_conversion t
| Lreal -> real_conversion t
| Ltype ({lt_name = name},[]) when name = Utf8_logic.boolean ->
bool_conversion t
@@ -400,7 +400,7 @@ let float_builtin prefix fkind =
| [ lf ] -> Some lf
| _ -> Kernel.fatal "Missing or ambiguous builtin %S" name
-let is_float_binop op typ =
+let get_float_binop op typ =
match typ, op with
| TFloat(fkind,_) , PlusA -> float_builtin "add" fkind
| TFloat(fkind,_) , MinusA -> float_builtin "sub" fkind
@@ -408,7 +408,7 @@ let is_float_binop op typ =
| TFloat(fkind,_) , Div -> float_builtin "div" fkind
| _ -> None
-let is_float_unop op typ =
+let get_float_unop op typ =
match typ, op with
| TFloat(fkind,_) , Neg -> float_builtin "neg" fkind
| _ -> None
@@ -419,7 +419,7 @@ let rec expr_to_term ?(coerce=false) e =
let ctyp = Ctype typ in
let node,ltyp =
match e.enode with
- | Const c -> TConst (constant_to_lconstant c) , coerced typ
+ | Const c -> TConst (constant_to_lconstant c) , coerce_type typ
| StartOf lv -> TStartOf (lval_to_term_lval lv) , ctyp
| AddrOf lv -> TAddrOf (lval_to_term_lval lv) , ctyp
| BinOp (op, a, b, _) ->
@@ -427,7 +427,7 @@ let rec expr_to_term ?(coerce=false) e =
let tc = expr_to_boolean e in
Tif( tc , Cil.lone ~loc () , Cil.lzero ~loc () ),
Linteger
- else begin match is_float_binop op typ with
+ else begin match get_float_binop op typ with
| Some phi ->
let va = expr_to_term a in
let vb = expr_to_term b in
@@ -435,20 +435,20 @@ let rec expr_to_term ?(coerce=false) e =
| None ->
let va = expr_to_term ~coerce:true a in
let vb = expr_to_term ~coerce:true b in
- TBinOp(op,va,vb) , coerced typ
+ TBinOp(op,va,vb) , coerce_type typ
end
| UnOp (LNot, c, _) ->
let tc = expr_to_boolean c in
Tif( tc , Cil.lzero ~loc () , Cil.lone ~loc () ),
Linteger
| UnOp(op, a, _) ->
- begin match is_float_unop op typ with
+ begin match get_float_unop op typ with
| Some phi ->
let va = expr_to_term ~coerce:true a in
Tapp(phi,[],[va]) , ctyp
| None ->
let va = expr_to_term ~coerce:true a in
- TUnOp(op,va) , coerced typ
+ TUnOp(op,va) , coerce_type typ
end
| SizeOf t -> TSizeOf t, ctyp
| SizeOfE e -> TSizeOf (Cil.typeOf e), ctyp
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 25dff3363f4..6f37795a6e9 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -86,7 +86,7 @@ val logicCType : logic_type -> typ
val array_to_ptr : logic_type -> logic_type
(** C type to logic type, with implicit conversion for arithmetic types. *)
-val coerced : typ -> logic_type
+val coerce_type : typ -> logic_type
(** {2 Predicates} *)
@@ -160,17 +160,17 @@ val pointer_comparable: ?loc:location -> term -> term -> predicate
(** {2 Conversion from exp to term} *)
val expr_to_term : ?coerce:bool -> exp -> term
-(** Returns a logic term that has exactly the same semantics than the
+(** Returns a logic term that has exactly the same semantics as the
original C-expression. The type of the resulting term is determined
by the [~coerce] flag as follows:
- when [~coerce:false] is given (the default) the term has the same
- c-type than the original expression.
+ c-type as the original expression.
- when [~coerce:true] is given, if the original expression has an int or
float type, then the returned term is coerced into the integer or real
logic type, respectively.
Remark: when the original expression is a comparison, it is evaluated as
- a [_Bool] or [integer] depending on the [~coerce] flag.
+ an [int] or an [integer] depending on the [~coerce] flag.
To obtain a boolean or predicate, use [expr_to_boolean] or
[expr_to_predicate] instead.
@@ -181,7 +181,7 @@ val expr_to_predicate: exp -> predicate
(** Returns a predicate semantically equivalent to the condition
of the original C-expression.
- This is different than [expr_to_term e |> scalar_term_to_predicate]
+ This is different from [expr_to_term e |> scalar_term_to_predicate]
since it directly translate C-relations into logic ones.
@raise Fatal error if the expression is not a comparison and cannot be
@@ -206,7 +206,7 @@ val expr_to_boolean: exp -> term
(** Returns a boolean term semantically equivalent to the condition
of the original C-expression.
- This is different than [expr_to_term e |> scalar_term_to_predicate]
+ This is different from [expr_to_term e |> scalar_term_to_predicate]
since it directly translate C-relations into logic ones.
@raise Fatal error if the expression is not a comparison and cannot be
--
GitLab