Rename Cil_builtins.is_builtin to be less misleading

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, _, _) ->

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 ?*)

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 *)
 

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

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)
 

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

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

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;

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 =