diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index 96deb0afdae6330f7d383b4a44339077ae9435f0..9c4ebad617365527cf71277e10a5884b17703b79 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -277,7 +277,7 @@ let warn_if_another_compiler_builtin name =
depends on Ast_info *)
let on_call_to_undeclared_function vi =
let name = vi.Cil_types.vname in
- if not (Ast_info.is_frama_c_builtin name) then begin
+ if not (Ast_info.start_with_frama_c_builtin name) then begin
if not (warn_if_another_compiler_builtin name) then
Kernel.warning ~wkey:Kernel.wkey_implicit_function_declaration
~current:true ~once:true
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index aba019286b2148db0fc9d9689ff377d4bc3298dc..6f159f16bb6af7a9686a30e25c573f57e0cf7082 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -173,7 +173,7 @@ class visitor = object(self)
Error.assigns_non_ghost_lvalue ~current:true lv
in
let is_builtin vi =
- Ast_info.is_frama_c_builtin vi.vname ||
+ Ast_info.start_with_frama_c_builtin vi.vname ||
Cil_builtins.is_builtin vi
in
let failed = match i with
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index 5030a6d76bd152f57382bd79873086bc11eed9b9..5c49b7a54704a590d4b598f163e5fde059325675 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -465,33 +465,33 @@ let pointed_type ty =
(** {2 Predefined} *)
(* ************************************************************************** *)
-let can_be_cea_function name =
- String.starts_with ~prefix:"Frama_" name
+let start_with_frama_c name =
+ String.starts_with ~prefix:"Frama_C_" name
-let is_cea_function name =
+let is_show_each_builtin name =
String.starts_with ~prefix:"Frama_C_show_each" name
-let is_cea_domain_function name =
+let is_domain_show_each_builtin name =
String.starts_with ~prefix:"Frama_C_domain_show_each" name
-let is_cea_dump_function name =
+let is_dump_each_builtin name =
String.starts_with ~prefix:"Frama_C_dump_each" name
-let is_cea_dump_file_function name =
+let is_dump_file_builtin name =
String.starts_with ~prefix:"Frama_C_dump_each_file" name
-let is_cea_builtin name =
- String.starts_with ~prefix:"Frama_C_builtin" name
+let is_split_builtin name =
+ String.starts_with ~prefix:"Frama_C_builtin_split" name
-let is_frama_c_builtin n =
- can_be_cea_function n &&
- (is_cea_dump_function n ||
- is_cea_function n ||
- is_cea_builtin n ||
- is_cea_domain_function n ||
- is_cea_dump_file_function n)
+let start_with_frama_c_builtin n =
+ start_with_frama_c n &&
+ (is_dump_each_builtin n ||
+ is_show_each_builtin n ||
+ is_split_builtin n ||
+ is_domain_show_each_builtin n ||
+ is_dump_file_builtin n)
-let () = Cil_builtins.add_special_builtin_family is_frama_c_builtin
+let () = Cil_builtins.add_special_builtin_family start_with_frama_c_builtin
(*
Local Variables:
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index b068cb7fac8bb92949e2f65de23804d936f63c43..f1284573e29f27e6c4de66fedd84f318b50deff6 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -240,12 +240,40 @@ end
(** {2 Predefined} *)
(* ************************************************************************** *)
-val can_be_cea_function : string -> bool
-val is_cea_function : string -> bool
-val is_cea_domain_function : string -> bool
-val is_cea_dump_function : string -> bool
-val is_cea_dump_file_function : string -> bool
-val is_frama_c_builtin : string -> bool
+val start_with_frama_c: string -> bool
+(** @return true if the given string starts with ["Frama_C_"].
+ @since Frama-C+dev
+*)
+
+val is_show_each_builtin: string -> bool
+(** @return true if the given string starts with ["Frama_C_show_each"].
+ @since Frama-C+dev
+*)
+
+val is_domain_show_each_builtin: string -> bool
+(** @return true if the given string starts with ["Frama_C_domain_show_each"].
+ @since Frama-C+dev
+*)
+
+val is_dump_each_builtin: string -> bool
+(** @return true if the given string starts with ["Frama_C_dump_each"].
+ @since Frama-C+dev
+*)
+
+val is_dump_file_builtin: string -> bool
+(** @return true if the given string starts with ["Frama_C_dump_each_file"].
+ @since Frama-C+dev
+*)
+
+val is_split_builtin: string -> bool
+(** @return true if the given string starts with ["Frama_C_builtin_split"].
+ @since Frama-C+dev
+*)
+
+val start_with_frama_c_builtin: string -> bool
+(** @return true if the given string starts with ["Frama_C_"].
+ @since Frama-C+dev
+*)
(*
Local Variables:
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 262a40268e873206e5d593f5b673c4280092ad51..891a2394b1970e1e017adeed3274f822dcfcaea6 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -177,7 +177,7 @@ module Base_checker = struct
let unknown () =
check_abort "variable %s(%d) is not declared" v.vname v.vid
in
- if not v.vglob || not (Ast_info.is_frama_c_builtin v.vname) then
+ if not v.vglob || not (Ast_info.start_with_frama_c_builtin v.vname) then
(try
if Varinfo.Hashtbl.find known_vars v != v then not_shared ()
with Not_found -> unknown ()
diff --git a/src/plugins/eva/engine/function_calls.ml b/src/plugins/eva/engine/function_calls.ml
index ee88bbdc58569980f49e7cbca5c5c539ca06cdeb..5b8cd029a76e9302b0b46e434645ee209704b11d 100644
--- a/src/plugins/eva/engine/function_calls.ml
+++ b/src/plugins/eva/engine/function_calls.ml
@@ -146,7 +146,7 @@ let analysis_status kf =
(* Must be consistent with the choice made by [analysis_target] below. *)
let use_spec_instead_of_definition ?(recursion_depth = -1) kf =
- Ast_info.is_frama_c_builtin (Kernel_function.get_name kf) ||
+ Ast_info.start_with_frama_c_builtin (Kernel_function.get_name kf) ||
Builtins.is_builtin_overridden kf ||
recursion_depth >= Parameters.RecursiveUnroll.get () ||
not (Kernel_function.is_definition kf) ||
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 1bb0994dc6e1d37e40f2327b477b4a1df71ad98a..34a7b67ef1f8590dd7a6a5ea37dc447b8ca7104e 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -85,7 +85,7 @@ let do_copy_at = function
let is_determinate kf =
let name = Kernel_function.get_name kf in
(warn_indeterminate kf || Function_calls.use_spec_instead_of_definition kf)
- && not (Ast_info.is_frama_c_builtin name)
+ && not (Ast_info.start_with_frama_c_builtin name)
let subdivide_stmt = Eva_utils.get_subdivision
@@ -708,15 +708,15 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(** Applies the show_each or dump_each directives. *)
let apply_special_directives ~subdivnb kf arguments state =
let name = Kernel_function.get_name kf in
- if Ast_info.can_be_cea_function name
+ if Ast_info.start_with_frama_c name
then
- if Ast_info.is_cea_function name
+ if Ast_info.is_show_each_builtin name
then (show_each ~subdivnb name arguments state; true)
- else if Ast_info.is_cea_domain_function name
+ else if Ast_info.is_domain_show_each_builtin name
then (domain_show_each ~subdivnb name arguments state; true)
- else if Ast_info.is_cea_dump_file_function name
+ else if Ast_info.is_dump_file_builtin name
then (dump_state_file ~subdivnb name arguments state; true)
- else if Ast_info.is_cea_dump_function name
+ else if Ast_info.is_dump_each_builtin name
then (dump_state name state; true)
else false
else false
diff --git a/src/plugins/eva/partitioning/auto_loop_unroll.ml b/src/plugins/eva/partitioning/auto_loop_unroll.ml
index 58b52807752271e0a9c58bb69d832deeb6f78844..fca0c44ebc07734543e871f4d45fa8be744cf173 100644
--- a/src/plugins/eva/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/eva/partitioning/auto_loop_unroll.ml
@@ -177,7 +177,7 @@ let add_written_var vi effect =
let is_frama_c_builtin exp =
match exp.enode with
- | Lval (Var vi, NoOffset) -> Ast_info.is_frama_c_builtin vi.vname
+ | Lval (Var vi, NoOffset) -> Ast_info.start_with_frama_c_builtin vi.vname
| _ -> false
let compute_instr_effect effect = function
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 4060d0d518378c27d35ebfd9724579e3e3f6354a..4c662872580ba2732f0583f403dda70ffe646c7a 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -346,7 +346,7 @@ struct
let states_with_formals = ref [] in
let do_on kf =
let called_vinfo = Kernel_function.get_vi kf in
- if Ast_info.is_frama_c_builtin called_vinfo.vname then
+ if Ast_info.start_with_frama_c_builtin called_vinfo.vname then
state
else
let froms_call = To_Use.get_from_call kf stmt in
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 3f874465f59b47884281ad734ce6e00f19b98259..a873fdbf6f894e4b03faea6bdaded41d0c61d0da 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -43,7 +43,7 @@ let all_properties () =
match Property.get_kf ip with
| None -> globals := Property.Set.add ip !globals
| Some kf ->
- if not (Ast_info.is_frama_c_builtin (Kernel_function.get_name kf))
+ if not (Ast_info.start_with_frama_c_builtin (Kernel_function.get_name kf))
then try
let fips = Kernel_function.Map.find kf !functions in
fips := Property.Set.add ip !fips
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index b20821d6b8dfc2fbdccfbd0c2ecfa44a9f66d9df..777bce0fd9b012002a2b9da61bb378a01dad7207 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -367,7 +367,7 @@ let get_filename fdef =
let consider_function ~libc vinfo =
not (Eva.Builtins.is_builtin vinfo.vname
- || Ast_info.is_frama_c_builtin vinfo.vname
+ || Ast_info.start_with_frama_c_builtin vinfo.vname
|| Cil_builtins.is_unused_builtin vinfo
) && (libc || not (Cil.is_in_libc vinfo.vattr))
diff --git a/src/plugins/report/scan.ml b/src/plugins/report/scan.ml
index 522d3376dddb4c87dfd1fcf7be3625996a5b3c4c..e7c28026e6a13de377f8e617906f036c57b8399a 100644
--- a/src/plugins/report/scan.ml
+++ b/src/plugins/report/scan.ml
@@ -126,7 +126,7 @@ let iter (inspector:inspector) =
match Property.get_kf ip with
| None -> globals := Property.Set.add ip !globals
| Some kf ->
- if not (Ast_info.is_frama_c_builtin (Kernel_function.get_name kf))
+ if not (Ast_info.start_with_frama_c_builtin (Kernel_function.get_name kf))
then try
let fips = Kernel_function.Map.find kf !functions in
fips := Property.Set.add ip !fips
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 02f8d10d536283f588b0daca43e8f97a0aa45050..c92bf683b585155d67ef88c99292989ecde548e7 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -170,7 +170,7 @@ class annot_visitor kf flags on_alarm = object (self)
match funcexp.enode with
| Lval (Var vinfo, NoOffset) ->
let kf = Globals.Functions.get vinfo in
- let frama_b = Ast_info.is_frama_c_builtin (Kernel_function.get_name kf)
+ let frama_b = Ast_info.start_with_frama_c_builtin (Kernel_function.get_name kf)
in
let va_start = Kernel_function.get_name kf = "__builtin_va_start" in
(frama_b, va_start)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 46a17d9e1422e7e5d1569cf3da7cf30b5291bd8f..0128d7e8bbe9cc86363a7291ed01efc65bf7992b 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -618,7 +618,7 @@ struct
Globals.Functions.iter
(fun kf ->
let name = Kernel_function.get_name kf in
- if not (Ast_info.is_frama_c_builtin name) then f kf)
+ if not (Ast_info.start_with_frama_c_builtin name) then f kf)
let array : kernel_function States.array =
begin
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 57d3d0305f4bfaa0aaf686adb88ccdae1f3d18ba..b7e821e4906a83172ef293c0de6fd5a6b36723eb 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -308,7 +308,7 @@ let is_relevant ip =
match Property.get_kf ip with
| None -> true
| Some kf ->
- not (Ast_info.is_frama_c_builtin (Kernel_function.get_name kf)
+ not (Ast_info.start_with_frama_c_builtin (Kernel_function.get_name kf)
|| Cil_builtins.is_unused_builtin (Kernel_function.get_vi kf))
let iter f =
diff --git a/src/plugins/variadic/classify.ml b/src/plugins/variadic/classify.ml
index 32d4c8c2c3690afd523cc768515874f2ba7813f3..7717ee908379ed0e830a06ec4b92ec6be8d108d2 100644
--- a/src/plugins/variadic/classify.ml
+++ b/src/plugins/variadic/classify.ml
@@ -111,7 +111,7 @@ let mk_format_fun vi f_kind f_buffer ~format_pos =
(* ************************************************************************ *)
let is_frama_c_builtin name =
- Ast_info.is_frama_c_builtin name ||
+ Ast_info.start_with_frama_c_builtin name ||
Cil_builtins.Builtin_functions.mem name ||
String.starts_with ~prefix:"__FRAMAC_" name (* Mthread prefixes *)