diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml index dd19bebde391fa347ec9cc07fe07b537c3fa8426..c80b32e7484b1a703e85d748253a8919524fe330 100644 --- a/src/kernel_services/ast_queries/cil_builtins.ml +++ b/src/kernel_services/ast_queries/cil_builtins.ml @@ -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 270cfd97d9e8fdf9e457c8bfc98f47f703c5680e..c37b7e41c8608f04e96c5cf38d480a0aea8abc4b 100644 --- a/src/kernel_services/ast_queries/cil_builtins.mli +++ b/src/kernel_services/ast_queries/cil_builtins.mli @@ -56,10 +56,15 @@ open Cil_types module Frama_c_builtins: State_builder.Hashtbl with type key = string and type data = varinfo -val is_frama_c_builtin: varinfo -> bool -(** @return true if the given variable refers to a Frama-C builtin. +val is_builtin: varinfo -> bool +(** @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 refers to a Frama-C builtin. + @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/plugins/eva/utils/summary.ml b/src/plugins/eva/utils/summary.ml index 84d99db49cbe95df0ec42b7f7540387539887ce6..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.has_fc_builtin_attr 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/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml index e497fb82648643c7176fa5586772a2cad0e5f7bd..fba8a49e215abae7019981c079bb1fca1763026a 100644 --- a/src/plugins/obfuscator/obfuscate.ml +++ b/src/plugins/obfuscator/obfuscate.ml @@ -101,8 +101,7 @@ class visitor = object else begin if Cil.isFunctionType vi.vtype then begin if vi.vname <> "main" - && not (Cil_builtins.has_fc_builtin_attr vi) - && not (Cil_builtins.is_special_builtin vi.vname) + && not (Cil_builtins.is_builtin vi) && not (Cil.is_in_libc vi.vattr) then vi.vname <- Dictionary.fresh Obfuscator_kind.Function vi.vname end