From 3c452827d7c6ed9c7a6ca598f44768ff7a28d340 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 23 Dec 2020 23:09:25 +0100
Subject: [PATCH] [Kernel] move is_in_libc from Metrics to Cil; add
global_is_in_libc
---
src/kernel_services/ast_queries/cil.ml | 7 +++++++
src/kernel_services/ast_queries/cil.mli | 12 ++++++++++++
src/plugins/metrics/metrics_base.ml | 9 +++------
3 files changed, 22 insertions(+), 6 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index fd327796b0b..7b508abd4af 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 4b74ee936bb..3f3e1b90794 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 6bbea44d76f..e1cc6633a3a 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
--
GitLab