Add is_frama_c_builtin: checks FC attr and start_with_Frama_C

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.start_with_frama_c_builtin vi.vname ||
-        Cil_builtins.has_fc_builtin_attr 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

src/kernel_services/ast_queries/ast_info.ml

@@ -491,6 +491,9 @@ let start_with_frama_c_builtin n =
    is_domain_show_each_builtin n ||
    is_dump_file_builtin n)
 
+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 start_with_frama_c_builtin
 
 (*

src/kernel_services/ast_queries/ast_info.mli

@@ -275,6 +275,12 @@ val start_with_frama_c_builtin: string -> bool
     @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:
 compile-command: "make -C ../../.."