diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml index 67a7a15ad9aae7985ba9a3998bff363a34ee4562..dd260448133df9396c39b2a93c1e98ba53f08be9 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 4bc65d57621c0a9b55781d84375b210e71206629..60cae71fd149e6c52cdb5015d2509e6194a17bb5 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 387c97650ecf978668b2b2cd9d8347631588b13e..88dc82d6538964a15a5d664d9bbb345c55e59d4d 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