diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 4c8f43f3d8aa503737740d4af436769737b767e7..132d30d68c5e67a30f5ee892952e95ba6a38a3c0 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 f39332dfbd8e58788cd8cf63424d606c16af3296..cb016440a6ce183d18b3732dd68c6bbf700b15ec 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 7d43c5cb2aac0210cf28e992340746724eb7d86b..072c245325c87aa19ce8e08e782c8407da1fc4d3 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 e688ca723c4e4593178251c30ee536b508d59467..ea9da3c02c4f8ac3c9495b978bc815759bcc82ca 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 2ee6847b25d290ca8c6aaf871a2303ea7572505b..c11f27519b99259adde35f7ba9d2d9965adf71b3 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 adf3a68221646a5e5ec2e086c1881840c05b88ec..78c7105fe3e4e427486d9eb47a826ff0e0c026c8 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 190deb18e576daa29788328186cc7a57c88bcf1e..4c5051422b7f219dc3a8c4aab69e1c262e088611 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 2bbe125a610fa13f0c632f1e3afff9b207bd7ac9..e2a72839350ab113656827bb2ccccea3ae867ddb 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 23b1d1dbac4fedc925047c3a2254092056d320a5..33fc8fc4c3abc07ded45489725070c179790d20e 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 8573642195cac4b0701a71bc726642759e15decc..5b5ed54e071b9898aa542ab3ca6542c05fac722f 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 62539f594e42587fbaf01d4fdddd3bf50b0012c6..b8b8e8f1dbf3dbc1754fb58b2fe825196bdb2eed 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 0432d1d2785b88e6baa85fae55ed024218b11be1..466dfd85c3670e535458db438b935ea46340ea20 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 fe7eba811ec90b257007807bf5e84be6c6bde9dd..9f3629c6a1ed1f7bf17b731f78e9be648e97fb8b 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 ef3514c844b85d222bb7e2cb5142a3b9dca67e02..5b44ee61a5da89feff5d5c2e5d9ecd77bca94223 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)