diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml index c125b5be59ee876651bb4f0020e9657a714e1b8c..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.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 diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml index 5c49b7a54704a590d4b598f163e5fde059325675..794763d3e27de46650aefce306562cc2b13fb5af 100644 --- a/src/kernel_services/ast_queries/ast_info.ml +++ b/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 (* diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli index f1284573e29f27e6c4de66fedd84f318b50deff6..771f071232a5cf47d5b2d2feb75f59bb744021a2 100644 --- a/src/kernel_services/ast_queries/ast_info.mli +++ b/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 ../../.."