Commit 3f90c01f authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

[Kernel] add `Annotations.has_funspec`

parent 84533c79
......@@ -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
......
......@@ -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.
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment