diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml index e9773fec250244714e8c02dfeaca029a662e3cef..0e5531c75fa63541da0978e6068fe12bb1b56301 100644 --- a/src/kernel_internals/typing/populate_spec.ml +++ b/src/kernel_internals/typing/populate_spec.ml @@ -96,7 +96,8 @@ let compare_it it1 it2 = Cil_datatype.Term.compare it1.it_content it2.it_content let is_frama_c_builtin kf = - Kernel_function.get_name kf |> Ast_info.is_frama_c_builtin + Kernel_function.get_vi kf |> Cil_builtins.is_builtin + ||Kernel_function.get_name kf |> Cil_builtins.is_special_builtin let is_frama_c_stdlib kf = (Kernel_function.get_vi kf).vattr |> Cil.is_in_libc