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..3d017490d7d37b0099814ee2fd6e4e67ef584c78 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -172,22 +172,18 @@ class visitor = object(self)
if not (isGhostType (typeOfLval lv)) then
Error.assigns_non_ghost_lvalue ~current:true lv
in
- let is_builtin vi =
- Ast_info.is_frama_c_builtin vi.vname ||
- Cil_builtins.is_builtin vi
- in
let failed = match i with
| Call(_, fexp, _, _) ->
begin match Kernel_function.(Option.map get_vi @@ get_called fexp) with
| Some fct
- when not (is_builtin fct) && not fct.vghost ->
+ when not (Ast_info.is_frama_c_builtin fct) && not fct.vghost ->
Error.non_ghost_function_call_in_ghost ~current:true () ; true
| None ->
Error.function_pointer_call ~current:true () ; true
| _ -> false
end
| Local_init(_, ConsInit(fct, _, _), _)
- when not (is_builtin fct) && not fct.vghost ->
+ when not (Ast_info.is_frama_c_builtin fct) && not fct.vghost ->
Error.non_ghost_function_call_in_ghost ~current:true () ; true
| _ -> false
in
@@ -200,10 +196,10 @@ class visitor = object(self)
| Call(_, fexp, _, _) ->
let vi =
Kernel_function.(get_vi @@ Option.get @@ get_called fexp) in
- if not (is_builtin vi) then
+ if not (Ast_info.is_frama_c_builtin vi) then
error_if_incompatible lv (getReturnType (typeOf fexp)) fexp
| Local_init(_, ConsInit(fct, _, _), _) ->
- if not (is_builtin fct) then
+ if not (Ast_info.is_frama_c_builtin fct) then
error_if_incompatible lv (getReturnType fct.vtype) (evar fct)
| _ -> ()
end
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index 5030a6d76bd152f57382bd79873086bc11eed9b9..b9da577467a961ca1a8e3b2c7ebbaf1cd577df51 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -465,33 +465,37 @@ 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 start_with_frama_c_builtin
+
+let is_frama_c_builtin v =
+ Cil_builtins.has_fc_builtin_attr v || start_with_frama_c_builtin v.vname
-let () = Cil_builtins.add_special_builtin_family is_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..771f071232a5cf47d5b2d2feb75f59bb744021a2 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -240,12 +240,46 @@ 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
+*)
+
+val is_frama_c_builtin: varinfo -> bool
+(** @return true if {!start_with_frama_c_builtin} or
+ {!Cil_builtins.has_fc_builtin_attr} are true.
+ @before Frama-C+dev Behave like {!start_with_frama_c_builtin}.
+*)
(*
Local Variables:
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index a2cdec06341601b2e2f0602b099678f4e06a3532..c80b32e7484b1a703e85d748253a8919524fe330 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 ?*)
@@ -68,6 +68,9 @@ let special_builtins = Queue.create ()
let is_special_builtin s =
Queue.fold (fun res f -> res || f s) false special_builtins
+let is_builtin v =
+ has_fc_builtin_attr v || is_special_builtin v.vname
+
let add_special_builtin_family f = Queue.add f special_builtins
let add_special_builtin s =
diff --git a/src/kernel_services/ast_queries/cil_builtins.mli b/src/kernel_services/ast_queries/cil_builtins.mli
index 76902c6d59284cabc83ad806c5063dbe5fae9265..45b02173c47744a19146fab35cc6eff13c84dbf8 100644
--- a/src/kernel_services/ast_queries/cil_builtins.mli
+++ b/src/kernel_services/ast_queries/cil_builtins.mli
@@ -57,9 +57,14 @@ module Frama_c_builtins:
State_builder.Hashtbl with type key = string and type data = varinfo
val is_builtin: varinfo -> bool
-(** @return true if the given variable refers to a Frama-C builtin.
+(** @return true if {!has_fc_builtin_attr} or {!is_special_builtin} are true.
+ @before Frama-C+dev Only check for {!has_fc_builtin_attr}.
@since Fluorine-20130401 *)
+val has_fc_builtin_attr: varinfo -> bool
+(** @return true if the given variable has a FC_BUILTIN attribute
+ @since Frama-C+dev *)
+
val is_unused_builtin: varinfo -> bool
(** @return true if the given variable refers to a Frama-C builtin that
is not used in the current program. Plugins may (and in fact should)
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/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/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/eva/utils/summary.ml b/src/plugins/eva/utils/summary.ml
index b168b19625124b901ddcf2b86c184e9d0ee1c13f..6982ec1bfeef2b3ad812871677fbe05e8d79fc86 100644
--- a/src/plugins/eva/utils/summary.ml
+++ b/src/plugins/eva/utils/summary.ml
@@ -225,9 +225,7 @@ end
let consider_function vi =
vi.Cil_types.vdefined &&
- not (Cil_builtins.is_builtin vi
- || Cil_builtins.is_special_builtin vi.vname
- || Cil.is_in_libc vi.vattr)
+ not (Cil_builtins.is_builtin vi || Cil.is_in_libc vi.vattr)
let compute_events () =
let eva = Events.make () and kernel = Events.make () in
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/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index 777b2cfc05de6807ce65cbb9c2cf59d58de36fa2..fba8a49e215abae7019981c079bb1fca1763026a 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/src/plugins/obfuscator/obfuscate.ml
@@ -102,7 +102,6 @@ class visitor = object
if Cil.isFunctionType vi.vtype then begin
if vi.vname <> "main"
&& not (Cil_builtins.is_builtin 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
end
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..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
@@ -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 *)
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 =