diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index fd327796b0b2d13459f7fabe0f203da3d65ef50a..7b508abd4af526ce3c0bd61e766f17dc560899ff 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/src/kernel_services/ast_queries/cil.ml @@ -5362,6 +5362,13 @@ let global_attributes = function | GAnnot (gannot,_) -> global_annotation_attributes gannot | GAsm _ | GText _ -> [] +let is_in_libc attrs = + hasAttribute "fc_stdlib" attrs || + hasAttribute "fc_stdlib_generated" attrs + +let global_is_in_libc g = + is_in_libc (global_attributes g) + (***************************************************************************) (* Convert an expression into an attribute, if possible. Otherwise raise diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli index 4b74ee936bb7666e86ea6793117cbd0a11563fe3..3f3e1b9079453eb9eaa9c96da7c579c4106c4dd4 100644 --- a/src/kernel_services/ast_queries/cil.mli +++ b/src/kernel_services/ast_queries/cil.mli @@ -1392,6 +1392,18 @@ val global_annotation_attributes: global_annotation -> attributes *) val global_attributes: global -> attributes +(** + Whether the given attributes contain libc indicators. + @since Frama-C+dev +*) +val is_in_libc: attributes -> bool + +(** + Whether the given global contains libc indicators. + @since Frama-C+dev +*) +val global_is_in_libc: global -> bool + exception NotAnAttrParam of exp (* ************************************************************************* *) diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml index 6bbea44d76f2e70d36867519f9277b9094d7acc6..e1cc6633a3aaf5a0da94b4553690eb766ec501cc 100644 --- a/src/plugins/metrics/metrics_base.ml +++ b/src/plugins/metrics/metrics_base.ml @@ -301,11 +301,8 @@ let pretty_extern_vars fmt s = Pretty_utils.pp_iter ~pre:"@[" ~suf:"@]" ~sep:";@ " VInfoSet.iter Printer.pp_varinfo fmt s -let is_in_libc attrs = Cil.hasAttribute "fc_stdlib" attrs || - Cil.hasAttribute "fc_stdlib_generated" attrs - let is_entry_point vinfo times_called = - times_called = 0 && not vinfo.vaddrof && not (is_in_libc vinfo.vattr) + times_called = 0 && not vinfo.vaddrof && not (Cil.is_in_libc vinfo.vattr) ;; let number_entry_points fs = @@ -371,11 +368,11 @@ let consider_function ~libc vinfo = not (!Db.Value.mem_builtin vinfo.vname || Ast_info.is_frama_c_builtin vinfo.vname || Cil_builtins.is_unused_builtin vinfo - ) && (libc || not (is_in_libc vinfo.vattr)) + ) && (libc || not (Cil.is_in_libc vinfo.vattr)) let consider_variable ~libc vinfo = not (Cil.hasAttribute "FRAMA_C_MODEL" vinfo.vattr) && - (libc || not (is_in_libc vinfo.vattr)) + (libc || not (Cil.is_in_libc vinfo.vattr)) let float_to_string f = let s = Format.sprintf "%F" f in