diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index 6f159f16bb6af7a9686a30e25c573f57e0cf7082..c125b5be59ee876651bb4f0020e9657a714e1b8c 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 a2cdec06341601b2e2f0602b099678f4e06a3532..dd19bebde391fa347ec9cc07fe07b537c3fa8426 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 76902c6d59284cabc83ad806c5063dbe5fae9265..270cfd97d9e8fdf9e457c8bfc98f47f703c5680e 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 f7c2936976227b7b12cf90bf734420948c2cbd8a..7b03b13df7d378e548a91f90d82582817b14e24e 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 b168b19625124b901ddcf2b86c184e9d0ee1c13f..84d99db49cbe95df0ec42b7f7540387539887ce6 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 777b2cfc05de6807ce65cbb9c2cf59d58de36fa2..e497fb82648643c7176fa5586772a2cad0e5f7bd 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 0128d7e8bbe9cc86363a7291ed01efc65bf7992b..5e9c740f8e09959a733ce577ef7665e949604caf 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 13e0908d44a34f390fda0e5077b8266c8eea746a..b6956f0222f7088bb574c59cfee988e77121b4bd 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 b89b9009d34d9dc3f4a9b9fbecf6593eb6a3aca6..71eab2c4a2a414f9abe38e41eb366d5aa1169c78 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 =