Merge branch 'feature/andre/metrics-undefined-and-unspecified' into 'master'

[Metrics] split 'undef functions' into 'spec-only' and 'unspec and undef'

See merge request frama-c/frama-c!2848

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

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.

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/>@ \
                         @[&nbsp; %a@]@ <br/>@ <br/>@ \
-                        @{<span>Undefined function(s)@} (%d):@ <br/>@ \
+                        @{<span>Specified-only function(s)@} (%d):@ <br/>@ \
+                        @[&nbsp; %a@]@ <br>@ <br/>@ \
+                        @{<span>Undefined and unspecified function(s)@} (%d):@ <br/>@ \
                         @[&nbsp; %a@]@ <br>@ <br/>@ \
                         @{<span>'Extern' global variable(s)@} (%d):@ <br/>@ \
                         @[&nbsp; %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;

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

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)

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)

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)

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)

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)

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;

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)

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)

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)