From 3f90c01f9e5afea06671deffa9b1f59722f280ac Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 24 Sep 2020 16:21:37 +0200
Subject: [PATCH] [Kernel] add `Annotations.has_funspec`
---
src/kernel_services/ast_data/annotations.ml | 5 +++++
src/kernel_services/ast_data/annotations.mli | 4 ++++
src/plugins/metrics/metrics_cilast.ml | 13 +++----------
3 files changed, 12 insertions(+), 10 deletions(-)
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 67a7a15ad9a..dd260448133 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -480,6 +480,11 @@ let generic_funspec merge get ?emitter ?(populate=true) kf =
let funspec ?emitter ?populate kf =
generic_funspec merge_funspec ?emitter ?populate (fun x -> x) kf
+let has_funspec kf =
+ try
+ not (Cil.is_empty_funspec (funspec ~populate:false kf))
+ with No_funspec _ -> false
+
(* Do not share behaviors with outside world if there's a single emitter. *)
let behaviors =
generic_funspec merge_behaviors
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index 4bc65d57621..60cae71fd14 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -67,6 +67,10 @@ val funspec:
generated.
@raise No_funspec whenever the given function has no specification *)
+val has_funspec: kernel_function -> bool
+(** @return [true] iff the function has a non-empty specification.
+ @since Frama-C+dev *)
+
val behaviors:
?emitter:Emitter.t -> ?populate:bool -> kernel_function -> funbehavior list
(** Get the behaviors clause of the contract associated to the given function.
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 387c97650ec..88dc82d6538 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -343,16 +343,9 @@ class slocVisitor ~libc : sloc_visitor = object(self)
in
if vinfo.vdefined
then update_call_map fundef_calls
- else
- let has_spec =
- try
- let spec = Annotations.funspec ~populate:false (Globals.Functions.get vinfo) in
- spec <> Cil.empty_funspec ()
- with Annotations.No_funspec _ ->
- false
- in
- if has_spec then update_call_map funspec_calls
- else update_call_map fundecl_calls
+ else if Annotations.has_funspec (Globals.Functions.get vinfo)
+ then update_call_map funspec_calls
+ else update_call_map fundecl_calls
method! vinst i =
begin match i with
--
GitLab