From bfd60a348a518fab409fc9ea7627aa05f06831bd Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed, 3 Jul 2024 16:40:25 +0200
Subject: [PATCH] [kernel] Remove deprecated Cil.isArithmeticOrPointerType
function
---
src/kernel_services/ast_queries/cil.ml | 2 --
src/kernel_services/ast_queries/cil.mli | 5 -----
src/kernel_services/ast_queries/logic_utils.ml | 2 +-
src/plugins/eva/domains/cvalue/builtins_split.ml | 4 ++--
src/plugins/eva/domains/cvalue/cvalue_queries.ml | 2 +-
src/plugins/eva/domains/equality/equality_domain.ml | 4 ++--
src/plugins/eva/domains/offsm_domain.ml | 2 +-
src/plugins/eva/domains/symbolic_locs.ml | 2 +-
src/plugins/eva/engine/transfer_stmt.ml | 6 +++---
src/plugins/eva/legacy/eval_op.ml | 2 +-
src/plugins/eva/legacy/eval_terms.ml | 2 +-
src/plugins/from/from_compute.ml | 2 +-
src/plugins/inout/cumulative_analysis.ml | 2 +-
src/plugins/wp/RefUsage.ml | 2 +-
14 files changed, 16 insertions(+), 23 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 4c8f43f3d8a..132d30d68c5 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3597,8 +3597,6 @@ let isPointerType t =
(* ISO 6.2.5.21 *)
let isScalarType t = isArithmeticType t || isPointerType t
-let isArithmeticOrPointerType = isScalarType
-
(********** TRANSPARENT UNION ******)
(* Check if a type is a transparent union, and return the first field if it
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index f39332dfbd8..cb016440a6c 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -559,11 +559,6 @@ val isArithmeticType: typ -> bool
*)
val isScalarType: typ -> bool
-(** alias of isScalarType.
- @deprecated 22.0-Titanium use isScalarType instead
-*)
-val isArithmeticOrPointerType: typ -> bool
-
(** True if the argument is a logic arithmetic type (i.e. integer, enum or
floating point, either C or mathematical one. *)
val isLogicArithmeticType: logic_type -> bool
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 7d43c5cb2aa..072c245325c 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -246,7 +246,7 @@ let mk_cast ?loc ?(force=false) newt t =
(Ctype newt')
-> unroll_cast e
| TCast(true,Linteger,e)
- when Cil.isArithmeticOrPointerType newt'
+ when Cil.isScalarType newt'
-> unroll_cast e
| TCast(true,Lreal,e)
when Cil.isFloatingType newt'
diff --git a/src/plugins/eva/domains/cvalue/builtins_split.ml b/src/plugins/eva/domains/cvalue/builtins_split.ml
index e688ca723c4..ea9da3c02c4 100644
--- a/src/plugins/eva/domains/cvalue/builtins_split.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_split.ml
@@ -72,7 +72,7 @@ let warning warn s =
singleton location with an arithmetic type, and that it contains no more than
[max_card] elements. *)
let split_v ~warn lv state max_card =
- if Cil.isArithmeticOrPointerType lv.typ then
+ if Cil.isScalarType lv.typ then
let loc = Cvalue_queries.lval_to_loc state lv in
if Locations.Location_Bits.cardinal_zero_or_one loc.Locations.loc then
let v_indet = Cvalue.Model.find_indeterminate state loc in
@@ -132,7 +132,7 @@ let rec gather_lv_in_exp acc e =
and gather_lv_in_lv acc lv =
let (host, offset) = lv.node in
let acc =
- if Cil.isArithmeticOrPointerType lv.typ
+ if Cil.isScalarType lv.typ
then lv :: acc
else acc
in
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
index 2ee6847b25d..c11f27519b9 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
@@ -118,7 +118,7 @@ module Queries = struct
v, alarms
let extract_lval ~oracle:_ _context state lval loc =
- if Cil.isArithmeticOrPointerType lval.Eva_ast.typ
+ if Cil.isScalarType lval.Eva_ast.typ
then extract_scalar_lval state lval loc
else extract_aggregate_lval state lval loc
diff --git a/src/plugins/eva/domains/equality/equality_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml
index adf3a682216..78c7105fe3e 100644
--- a/src/plugins/eva/domains/equality/equality_domain.ml
+++ b/src/plugins/eva/domains/equality/equality_domain.ml
@@ -381,7 +381,7 @@ struct
let assign_eq left_lval right_expr value valuation state =
if Eva_ast.lval_contains_volatile left_lval ||
Eva_ast.exp_contains_volatile right_expr ||
- not (Cil.isArithmeticOrPointerType left_lval.typ) ||
+ not (Cil.isScalarType left_lval.typ) ||
indeterminate_copy value
then state
else
@@ -457,7 +457,7 @@ struct
and e2 = Eva_ast.const_fold e2 in
if Eva_ast.exp_contains_volatile e1
|| Eva_ast.exp_contains_volatile e2
- || not (Cil.isArithmeticOrPointerType e1.typ)
+ || not (Cil.isScalarType e1.typ)
|| (expr_is_cardinal_zero_or_one_loc valuation e1 &&
expr_cardinal_zero_or_one valuation e2)
|| (expr_is_cardinal_zero_or_one_loc valuation e2 &&
diff --git a/src/plugins/eva/domains/offsm_domain.ml b/src/plugins/eva/domains/offsm_domain.ml
index 190deb18e57..4c5051422b7 100644
--- a/src/plugins/eva/domains/offsm_domain.ml
+++ b/src/plugins/eva/domains/offsm_domain.ml
@@ -186,7 +186,7 @@ module D : Abstract_domain.Leaf
let extract_lval ~oracle:_ _context state lv locs =
let o =
if Cil.typeHasQualifier "volatile" lv.Eva_ast.typ ||
- not (Cil.isArithmeticOrPointerType lv.Eva_ast.typ)
+ not (Cil.isScalarType lv.Eva_ast.typ)
then
`Value (Top, None)
else
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index 2bbe125a610..e2a72839350 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -543,7 +543,7 @@ module D : Abstract_domain.Leaf
`Value (Memory.kill loc state)
let store_copy valuation lv loc state fv =
- if Cil.isArithmeticOrPointerType lv.lval.typ then
+ if Cil.isScalarType lv.lval.typ then
match fv.v, fv.initialized, fv.escaping with
| `Value v, true, false -> store_value valuation lv.lval loc state v
| _ -> store_indeterminate state loc
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 23b1d1dbac4..33fc8fc4c3a 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -365,7 +365,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let written_formals = Backward_formals.written_formals call.kf in
let is_safe argument =
not (Varinfo.Set.mem argument.formal written_formals)
- && Cil.isArithmeticOrPointerType argument.formal.vtype
+ && Cil.isScalarType argument.formal.vtype
&& is_safe_argument valuation argument.concrete
in
List.filter is_safe call.arguments
@@ -496,7 +496,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
Self.abort ~current:true
"Function argument %a has unknown size. Aborting"
Eva_ast.pp_exp expr;
- if determinate && Cil.isArithmeticOrPointerType lv.typ
+ if determinate && Cil.isScalarType lv.typ
then assign_by_eval ~subdivnb state valuation expr
else assign_by_copy ~subdivnb state valuation lv loc
| _ -> assign_by_eval ~subdivnb state valuation expr
@@ -645,7 +645,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(Bottom.pretty Cvalue.V.pretty) fmt value
let pretty_arguments ~subdivnb state arguments =
- let is_scalar lval = Cil.isArithmeticOrPointerType lval.Eva_ast.typ in
+ let is_scalar lval = Cil.isScalarType lval.Eva_ast.typ in
let pretty fmt (expr : Eva_ast.exp) =
match expr.node with
| Lval lval | StartOf lval when not (is_scalar lval) ->
diff --git a/src/plugins/eva/legacy/eval_op.ml b/src/plugins/eva/legacy/eval_op.ml
index 8573642195c..5b5ed54e071 100644
--- a/src/plugins/eva/legacy/eval_op.ml
+++ b/src/plugins/eva/legacy/eval_op.ml
@@ -191,7 +191,7 @@ let apply_on_all_locs f loc state =
(* Display [o] as a single value, when this is more readable and more precise
than the standard display. *)
let pretty_stitched_offsetmap fmt typ o =
- if Cil.isArithmeticOrPointerType typ &&
+ if Cil.isScalarType typ &&
not (Cvalue.V_Offsetmap.is_single_interval o)
then
let v = v_uninit_of_offsetmap ~typ o in
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 62539f594e4..b8b8e8f1dbf 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -508,7 +508,7 @@ let rec isLogicNonCompositeType t =
(try isLogicNonCompositeType (Logic_const.type_of_element t)
with Failure _ -> false)
| Linteger | Lreal -> true
- | Ctype t -> Cil.isArithmeticOrPointerType t
+ | Ctype t -> Cil.isScalarType t
let rec infer_type = function
| Ctype t ->
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 0432d1d2785..466dfd85c36 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -438,7 +438,7 @@ struct
padding bits. The 100 limit is arbitrary. *)
let implicit =
not (Cil.isArrayType ct &&
- (Cil.isArithmeticOrPointerType (Cil.typeOf_array_elem ct)
+ (Cil.isScalarType (Cil.typeOf_array_elem ct)
|| Ast_info.array_size ct > (Integer.of_int 100)))
in
let r = Cil.foldLeftCompound ~implicit ~doinit ~ct ~initl ~acc in
diff --git a/src/plugins/inout/cumulative_analysis.ml b/src/plugins/inout/cumulative_analysis.ml
index fe7eba811ec..9f3629c6a1e 100644
--- a/src/plugins/inout/cumulative_analysis.ml
+++ b/src/plugins/inout/cumulative_analysis.ml
@@ -32,7 +32,7 @@ open Visitor
let fold_implicit_initializer typ =
not
(Cil.isArrayType typ &&
- (Cil.isArithmeticOrPointerType (Cil.typeOf_array_elem typ)
+ (Cil.isScalarType (Cil.typeOf_array_elem typ)
|| Ast_info.array_size typ > (Integer.of_int 100)))
let specialize_state_on_call ?stmt kf =
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index ef3514c844b..5b44ee61a5d 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -215,7 +215,7 @@ let field = function
let load = function
| Loc_var x -> Val_var x (* E.access x ByValue E.bot *)
| Loc_shift(x,e) ->
- if Cil.isArithmeticOrPointerType x.vtype then
+ if Cil.isScalarType x.vtype then
E (E.access x ByAddr e)
else
E (E.access x ByValue e)
--
GitLab