From 18e9f78417d3c32ea79aae03d50cf910493866e1 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 28 Sep 2023 10:54:04 +0200
Subject: [PATCH] Rename Cil_builtins.is_builtin to be less misleading
---
src/kernel_internals/typing/ghost_accesses.ml | 2 +-
src/kernel_services/ast_queries/cil_builtins.ml | 4 ++--
src/kernel_services/ast_queries/cil_builtins.mli | 2 +-
src/plugins/e-acsl/src/libraries/misc.ml | 2 +-
src/plugins/eva/utils/summary.ml | 2 +-
src/plugins/obfuscator/obfuscate.ml | 2 +-
src/plugins/server/kernel_ast.ml | 2 +-
src/plugins/wp/RefUsage.ml | 4 +---
tests/misc/bts1347.ml | 2 +-
9 files changed, 10 insertions(+), 12 deletions(-)
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index 6f159f16bb6..c125b5be59e 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -174,7 +174,7 @@ class visitor = object(self)
in
let is_builtin vi =
Ast_info.start_with_frama_c_builtin vi.vname ||
- Cil_builtins.is_builtin vi
+ Cil_builtins.has_fc_builtin_attr vi
in
let failed = match i with
| Call(_, fexp, _, _) ->
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index a2cdec06341..dd19bebde39 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -56,9 +56,9 @@ module Frama_c_builtins =
let size = 3
end)
-let is_builtin v = Cil.hasAttribute "FC_BUILTIN" v.vattr
+let has_fc_builtin_attr v = Cil.hasAttribute "FC_BUILTIN" v.vattr
-let is_unused_builtin v = is_builtin v && not v.vreferenced
+let is_unused_builtin v = has_fc_builtin_attr v && not v.vreferenced
(* [VP] Should we projectify this ?*)
diff --git a/src/kernel_services/ast_queries/cil_builtins.mli b/src/kernel_services/ast_queries/cil_builtins.mli
index 76902c6d592..270cfd97d9e 100644
--- a/src/kernel_services/ast_queries/cil_builtins.mli
+++ b/src/kernel_services/ast_queries/cil_builtins.mli
@@ -56,7 +56,7 @@ open Cil_types
module Frama_c_builtins:
State_builder.Hashtbl with type key = string and type data = varinfo
-val is_builtin: varinfo -> bool
+val is_frama_c_builtin: varinfo -> bool
(** @return true if the given variable refers to a Frama-C builtin.
@since Fluorine-20130401 *)
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index f7c29369762..7b03b13df7d 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -27,7 +27,7 @@ open Cil_types
(* ************************************************************************** *)
let is_fc_or_compiler_builtin vi =
- Cil_builtins.is_builtin vi
+ Cil_builtins.has_fc_builtin_attr vi
||
(let prefix_length = 10 (* number of characters in "__builtin_" *) in
String.length vi.vname > prefix_length
diff --git a/src/plugins/eva/utils/summary.ml b/src/plugins/eva/utils/summary.ml
index b168b196251..84d99db49cb 100644
--- a/src/plugins/eva/utils/summary.ml
+++ b/src/plugins/eva/utils/summary.ml
@@ -225,7 +225,7 @@ end
let consider_function vi =
vi.Cil_types.vdefined &&
- not (Cil_builtins.is_builtin vi
+ not (Cil_builtins.has_fc_builtin_attr vi
|| Cil_builtins.is_special_builtin vi.vname
|| Cil.is_in_libc vi.vattr)
diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index 777b2cfc05d..e497fb82648 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/src/plugins/obfuscator/obfuscate.ml
@@ -101,7 +101,7 @@ class visitor = object
else begin
if Cil.isFunctionType vi.vtype then begin
if vi.vname <> "main"
- && not (Cil_builtins.is_builtin vi)
+ && not (Cil_builtins.has_fc_builtin_attr vi)
&& not (Cil_builtins.is_special_builtin vi.vname)
&& not (Cil.is_in_libc vi.vattr) then
vi.vname <- Dictionary.fresh Obfuscator_kind.Function vi.vname
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 0128d7e8bbe..5e9c740f8e0 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -608,7 +608,7 @@ struct
if not libc then Kernel.PrintLibc.set false ; raise err
let is_builtin kf =
- Cil_builtins.is_builtin (Kernel_function.get_vi kf)
+ Cil_builtins.has_fc_builtin_attr (Kernel_function.get_vi kf)
let is_extern kf =
let vi = Kernel_function.get_vi kf in
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 13e0908d44a..b6956f0222f 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -681,8 +681,6 @@ let cfun_spec env kf =
let cfun kf =
let env = mk_ctx () in
- (* Skipping frama-c builtins?
- if not (Cil_builtins.is_builtin (Kernel_function.get_vi kf)) then *)
begin
if Kernel_function.is_definition kf then cfun_code env kf ;
cfun_spec env kf
@@ -915,7 +913,7 @@ let dump () =
in Format.fprintf fmt "@[<hv 0>Init:@ %a@]@." E.pretty a_init ;
KFmap.iter (fun kf m ->
(* Do not dump results for frama-c builtins *)
- if not (Cil_builtins.is_builtin (Kernel_function.get_vi kf)) then
+ if not (Cil_builtins.has_fc_builtin_attr (Kernel_function.get_vi kf)) then
Format.fprintf fmt "@[<hv 0>Function %a:@ %a@]@."
Kernel_function.pretty kf E.pretty m ;
) a_usage;
diff --git a/tests/misc/bts1347.ml b/tests/misc/bts1347.ml
index b89b9009d34..71eab2c4a2a 100644
--- a/tests/misc/bts1347.ml
+++ b/tests/misc/bts1347.ml
@@ -5,7 +5,7 @@ let emitter =
let run () =
Globals.Functions.iter
(fun kf ->
- if not (Cil_builtins.is_builtin (Kernel_function.get_vi kf)) then begin
+ if not (Cil_builtins.has_fc_builtin_attr (Kernel_function.get_vi kf)) then begin
Globals.set_entry_point (Kernel_function.get_name kf) true;
Eva.Analysis.compute();
let hyps =
--
GitLab