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 e719e52e683d298406b5e70bed2f14c561ea5d3a..88dc82d6538964a15a5d664d9bbb345c55e59d4d 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -27,8 +27,9 @@ open Metrics_base
;;
type cilast_metrics = {
- fundecl_calls: int Metrics_base.VInfoMap.t;
- fundef_calls: int Metrics_base.VInfoMap.t;
+ fundecl_calls: int Metrics_base.VInfoMap.t; (* undefined and unspecified *)
+ funspec_calls: int Metrics_base.VInfoMap.t; (* undefined, but with spec *)
+ fundef_calls: int Metrics_base.VInfoMap.t; (* defined *)
extern_global_vars: Metrics_base.VInfoSet.t;
basic_global_metrics: BasicMetrics.t
}
@@ -43,9 +44,10 @@ class type sloc_visitor = object
inherit Visitor.generic_frama_c_visitor
(* Get the number of times a function has been called if it has been
- defined (fundef) or not (fundecl).
+ defined (fundef), specified (funspec), or just declared (fundecl).
*)
method fundecl_calls: int Metrics_base.VInfoMap.t
+ method funspec_calls: int Metrics_base.VInfoMap.t
method fundef_calls: int Metrics_base.VInfoMap.t
(* Global variables with 'Extern' storage *)
method extern_global_vars: Metrics_base.VInfoSet.t
@@ -92,11 +94,13 @@ class slocVisitor ~libc : sloc_visitor = object(self)
val mutable seen_vars = Varinfo.Set.empty;
val fundecl_calls: int VInfoMap.t ref = ref VInfoMap.empty;
+ val funspec_calls: int VInfoMap.t ref = ref VInfoMap.empty;
val fundef_calls: int VInfoMap.t ref = ref VInfoMap.empty;
val extern_global_vars = ref VInfoSet.empty
(* Getters/setters *)
method fundecl_calls = !fundecl_calls
+ method funspec_calls = !funspec_calls
method fundef_calls = !fundef_calls
method extern_global_vars = !extern_global_vars
method get_global_metrics = !global_metrics
@@ -339,9 +343,10 @@ class slocVisitor ~libc : sloc_visitor = object(self)
in
if vinfo.vdefined
then update_call_map fundef_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
| Call(v, e, _, _) ->
@@ -575,7 +580,9 @@ let dump_html fmt cil_visitor =
@{<h2>Synthetic results@}@ <br/>@ \
@{<span>Defined function(s)@} (%d): <br/>@ \
@[ %a@]@ <br/>@ <br/>@ \
- @{<span>Undefined function(s)@} (%d):@ <br/>@ \
+ @{<span>Specified-only function(s)@} (%d):@ <br/>@ \
+ @[ %a@]@ <br>@ <br/>@ \
+ @{<span>Undefined and unspecified function(s)@} (%d):@ <br/>@ \
@[ %a@]@ <br>@ <br/>@ \
@{<span>'Extern' global variable(s)@} (%d):@ <br/>@ \
@[ %a@]@ <br>@ <br/>@ \
@@ -584,6 +591,8 @@ let dump_html fmt cil_visitor =
@}@]"
(VInfoMap.cardinal cil_visitor#fundef_calls)
Metrics_base.pretty_set cil_visitor#fundef_calls
+ (VInfoMap.cardinal cil_visitor#funspec_calls)
+ Metrics_base.pretty_set cil_visitor#funspec_calls
(VInfoMap.cardinal cil_visitor#fundecl_calls)
Metrics_base.pretty_set cil_visitor#fundecl_calls
(VInfoSet.cardinal cil_visitor#extern_global_vars)
@@ -625,21 +634,26 @@ let dump_html fmt cil_visitor =
let pp_funinfo fmt vis =
let nfundef = VInfoMap.cardinal vis#fundef_calls in
+ let nfunspec = VInfoMap.cardinal vis#funspec_calls in
let nfundecl = VInfoMap.cardinal vis#fundecl_calls in
let nextern = VInfoSet.cardinal vis#extern_global_vars in
let fundef_hdr = Format.sprintf "Defined functions (%d)" nfundef
- and fundecl_hdr = Format.sprintf "Undefined functions (%d)" nfundecl
+ and funspec_hdr = Format.sprintf "Specified-only functions (%d)" nfunspec
+ and fundecl_hdr = Format.sprintf "Undefined and unspecified functions (%d)" nfundecl
and extern_hdr = Format.sprintf "'Extern' global variables (%d)" nextern
and entry_pts_hdr = Format.sprintf "Potential entry points (%d)"
(Metrics_base.number_entry_points vis#fundef_calls) in
Format.fprintf fmt
"@[<v 0>@[<v 1>%a@ @[%a@]@]@ @ \
+ @[<v 1>%a@ @[%a@]@]@ @ \
@[<v 1>%a@ @[%a@]@]@ @ \
@[<v 1>%a@ @[%a@]@]@ @ \
@[<v 1>%a@ @[%a@]@]@ \
@]"
(Metrics_base.mk_hdr 1) fundef_hdr
Metrics_base.pretty_set vis#fundef_calls
+ (Metrics_base.mk_hdr 1) funspec_hdr
+ Metrics_base.pretty_set vis#funspec_calls
(Metrics_base.mk_hdr 1) fundecl_hdr
Metrics_base.pretty_set vis#fundecl_calls
(Metrics_base.mk_hdr 1) extern_hdr
@@ -680,6 +694,7 @@ let get_cilast_metrics ~libc =
(cil_visitor:>Visitor.frama_c_visitor) file;
{
fundecl_calls = cil_visitor#fundecl_calls;
+ funspec_calls = cil_visitor#funspec_calls;
fundef_calls = cil_visitor#fundef_calls;
extern_global_vars = cil_visitor#extern_global_vars;
basic_global_metrics = cil_visitor#get_global_metrics;
diff --git a/src/plugins/metrics/metrics_cilast.mli b/src/plugins/metrics/metrics_cilast.mli
index 2da3fbdf04b2c1d4e1741b761d7a8cafcadafca2..e7dcd86abb58e8e9e5e8a9b9099a577fd08fe685 100644
--- a/src/plugins/metrics/metrics_cilast.mli
+++ b/src/plugins/metrics/metrics_cilast.mli
@@ -31,9 +31,10 @@ class type sloc_visitor = object
inherit Visitor.generic_frama_c_visitor
(* Get the number of times a function has been called if it has been
- defined (fundef) or not (fundecl).
+ defined (fundef), specified (funspec), or just declared (fundecl).
*)
method fundecl_calls: int Metrics_base.VInfoMap.t
+ method funspec_calls: int Metrics_base.VInfoMap.t
method fundef_calls: int Metrics_base.VInfoMap.t
method extern_global_vars: Metrics_base.VInfoSet.t
@@ -64,6 +65,7 @@ val get_global_metrics : libc:bool -> Metrics_base.BasicMetrics.t ;;
type cilast_metrics = {
fundecl_calls: int Metrics_base.VInfoMap.t;
+ funspec_calls: int Metrics_base.VInfoMap.t;
fundef_calls: int Metrics_base.VInfoMap.t;
extern_global_vars: Metrics_base.VInfoSet.t;
basic_global_metrics: Metrics_base.BasicMetrics.t
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 137fa9791933b936071c38736c51a369e8aba4ac..21143ee8813c382d58b61c64f175924430c33b18 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -41,8 +41,8 @@
wcscpy (0 call); wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call);
wmemcpy (0 call); wmemset (0 call);
- Undefined functions (412)
- =========================
+ Specified-only functions (411)
+ ==============================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
Frama_C_long_long_interval (0 call);
@@ -52,21 +52,21 @@
Frama_C_unsigned_long_interval (0 call);
Frama_C_unsigned_long_long_interval (0 call);
Frama_C_unsigned_short_interval (0 call); _Exit (0 call);
- __builtin_abort (1 call); __builtin_clz (0 call); __builtin_clzl (0 call);
- __builtin_clzll (0 call); __builtin_ctz (0 call); __builtin_ctzl (0 call);
- __builtin_ctzll (0 call); __builtin_popcount (0 call);
- __builtin_popcountl (0 call); __builtin_popcountll (0 call);
- __builtin_sadd_overflow (0 call); __builtin_saddl_overflow (0 call);
- __builtin_saddll_overflow (0 call); __builtin_smul_overflow (0 call);
- __builtin_smull_overflow (0 call); __builtin_smulll_overflow (0 call);
- __builtin_ssub_overflow (0 call); __builtin_ssubl_overflow (0 call);
- __builtin_ssubll_overflow (0 call); __builtin_uadd_overflow (0 call);
- __builtin_uaddl_overflow (0 call); __builtin_uaddll_overflow (0 call);
- __builtin_umul_overflow (0 call); __builtin_umull_overflow (0 call);
- __builtin_umulll_overflow (0 call); __builtin_usub_overflow (0 call);
- __builtin_usubl_overflow (0 call); __builtin_usubll_overflow (0 call);
- __fc_fpclassify (0 call); __fc_fpclassifyf (0 call); __fc_infinity (0 call);
- __fc_nan (0 call); __va_fcntl_flock (0 call); __va_fcntl_int (0 call);
+ __builtin_clz (0 call); __builtin_clzl (0 call); __builtin_clzll (0 call);
+ __builtin_ctz (0 call); __builtin_ctzl (0 call); __builtin_ctzll (0 call);
+ __builtin_popcount (0 call); __builtin_popcountl (0 call);
+ __builtin_popcountll (0 call); __builtin_sadd_overflow (0 call);
+ __builtin_saddl_overflow (0 call); __builtin_saddll_overflow (0 call);
+ __builtin_smul_overflow (0 call); __builtin_smull_overflow (0 call);
+ __builtin_smulll_overflow (0 call); __builtin_ssub_overflow (0 call);
+ __builtin_ssubl_overflow (0 call); __builtin_ssubll_overflow (0 call);
+ __builtin_uadd_overflow (0 call); __builtin_uaddl_overflow (0 call);
+ __builtin_uaddll_overflow (0 call); __builtin_umul_overflow (0 call);
+ __builtin_umull_overflow (0 call); __builtin_umulll_overflow (0 call);
+ __builtin_usub_overflow (0 call); __builtin_usubl_overflow (0 call);
+ __builtin_usubll_overflow (0 call); __fc_fpclassify (0 call);
+ __fc_fpclassifyf (0 call); __fc_infinity (0 call); __fc_nan (0 call);
+ __va_fcntl_flock (0 call); __va_fcntl_int (0 call);
__va_fcntl_void (0 call); __va_ioctl_int (0 call); __va_ioctl_ptr (0 call);
__va_ioctl_void (0 call); __va_open_mode_t (0 call);
__va_open_void (0 call); __va_openat_mode_t (0 call);
@@ -166,6 +166,10 @@
wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
wmemcmp (0 call); wmemmove (0 call); write (0 call);
+ Undefined and unspecified functions (1)
+ =======================================
+ __builtin_abort (1 call);
+
'Extern' global variables (16)
==============================
__fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_name;
@@ -280,8 +284,12 @@ void main(void)
=====================
main (0 call);
- Undefined functions (0)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (0)
+ =======================================
'Extern' global variables (0)
diff --git a/tests/metrics/oracle/cyclo_comp5.res.oracle b/tests/metrics/oracle/cyclo_comp5.res.oracle
index 835739a7ac6cccc22eecdb352c4ea99b49928ab3..18ec0102d5817e5f9701bf67541c40d797c46735 100644
--- a/tests/metrics/oracle/cyclo_comp5.res.oracle
+++ b/tests/metrics/oracle/cyclo_comp5.res.oracle
@@ -3,8 +3,12 @@
=====================
complexity5 (1 call); main (0 call);
- Undefined functions (1)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (1)
+ =======================================
printf (4 calls);
'Extern' global variables (0)
diff --git a/tests/metrics/oracle/func_ptr.0.res.oracle b/tests/metrics/oracle/func_ptr.0.res.oracle
index 0a380c923213a518b44cc5ab6df690031a0bcdcb..c9313069f7017731771703439bc1b8d1a9d802e3 100644
--- a/tests/metrics/oracle/func_ptr.0.res.oracle
+++ b/tests/metrics/oracle/func_ptr.0.res.oracle
@@ -6,8 +6,12 @@
baz (address taken) (0 call); foo (address taken) (0 call); foobar (0 call);
main (0 call);
- Undefined functions (1)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (1)
+ =======================================
exit (1 call);
'Extern' global variables (1)
diff --git a/tests/metrics/oracle/func_ptr.1.res.oracle b/tests/metrics/oracle/func_ptr.1.res.oracle
index b44df54a2fe98e9eaaf8914d44887efdcafcf7d7..740bbb61a1c4bcffd328590172adcbec43cfe192 100644
--- a/tests/metrics/oracle/func_ptr.1.res.oracle
+++ b/tests/metrics/oracle/func_ptr.1.res.oracle
@@ -6,8 +6,12 @@
baz (address taken) (0 call); foo (address taken) (0 call); foobar (0 call);
main (0 call);
- Undefined functions (1)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (1)
+ =======================================
exit (1 call);
'Extern' global variables (1)
diff --git a/tests/metrics/oracle/libc.0.res.oracle b/tests/metrics/oracle/libc.0.res.oracle
index c3bb5a741d5ae3a77120a0d2459ee3498e48cef0..1742799970db9aaf042da8cb6a6a88c3b2064fb1 100644
--- a/tests/metrics/oracle/libc.0.res.oracle
+++ b/tests/metrics/oracle/libc.0.res.oracle
@@ -4,8 +4,12 @@
bar (0 call); f (0 call); foo (0 call); g (address taken) (0 call);
main (0 call);
- Undefined functions (0)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (0)
+ =======================================
'Extern' global variables (0)
diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle
index b00598fd71aca4eccd755a531118a5da73a0c72a..690ea20f9c48ac4bf117fb98c399422473ffa09e 100644
--- a/tests/metrics/oracle/libc.1.res.oracle
+++ b/tests/metrics/oracle/libc.1.res.oracle
@@ -4,8 +4,8 @@
bar (1 call); f (0 call); foo (1 call); g (address taken) (0 call);
getopt (1 call); main (0 call);
- Undefined functions (122)
- =========================
+ Specified-only functions (122)
+ ==============================
_exit (0 call); access (0 call); chdir (0 call); chown (0 call);
chroot (0 call); clearerr (0 call); clearerr_unlocked (0 call);
close (0 call); dup (0 call); dup2 (0 call); execl (0 call);
@@ -40,6 +40,10 @@
vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
write (0 call);
+ Undefined and unspecified functions (0)
+ =======================================
+
+
'Extern' global variables (10)
==============================
Frama_C_entropy_source; __fc_errno; __fc_hostname; __fc_stdin; __fc_stdout;
diff --git a/tests/metrics/oracle/reach.res.oracle b/tests/metrics/oracle/reach.res.oracle
index 76558191ccef8ba929bce7f1571de2c98c5c21f7..f033a695ab9aa6e9b440e88781aa0ff4de62ebb3 100644
--- a/tests/metrics/oracle/reach.res.oracle
+++ b/tests/metrics/oracle/reach.res.oracle
@@ -49,8 +49,12 @@
=====================
baz (address taken) (0 call); foo (address taken) (0 call); main (0 call);
- Undefined functions (0)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (0)
+ =======================================
'Extern' global variables (0)
diff --git a/tests/metrics/oracle/unreachable.res.oracle b/tests/metrics/oracle/unreachable.res.oracle
index 38770a200d191a2cfe6964fe6a343e78ba57eef8..f3507cf43c937e3799a3adc71258902979d0968e 100644
--- a/tests/metrics/oracle/unreachable.res.oracle
+++ b/tests/metrics/oracle/unreachable.res.oracle
@@ -3,8 +3,12 @@
=====================
foo (1 call); main (0 call);
- Undefined functions (0)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (0)
+ =======================================
'Extern' global variables (0)
diff --git a/tests/metrics/oracle/variadic-stdlib-generated.res.oracle b/tests/metrics/oracle/variadic-stdlib-generated.res.oracle
index e79acc9295d1898d0dd001cc456ccf3a46b2f438..edae7ad63d89c6742e2a2bc06295435ce87334e7 100644
--- a/tests/metrics/oracle/variadic-stdlib-generated.res.oracle
+++ b/tests/metrics/oracle/variadic-stdlib-generated.res.oracle
@@ -3,8 +3,12 @@
=====================
main (0 call); my_printf (1 call);
- Undefined functions (1)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (1)
+ =======================================
rand (1 call);
'Extern' global variables (0)