Commit 854d2365 authored by Virgile Prevosto's avatar Virgile Prevosto

Merge branch 'feature/andre/metrics-json-output' into 'master'

[Metrics] add (partial) support for JSON output

See merge request frama-c/frama-c!2894
parents 0aab40cd 8d5841a1
......@@ -52,6 +52,7 @@ autom4te.cache
/tests/crowbar/mutable
/tests/crowbar/output-*
/tests/crowbar/test_ghost_cfg
/tests/fc_script/compile_commands.json
/tests/journal/intra.byte
/tests/misc/my_visitor_plugin/my_visitor.opt
/tests/misc/my_visitor.sav
......
......@@ -1072,8 +1072,8 @@ the sequence above is read in order and defines a configuration level
\texttt{CMD}\nscodeidx{Test!Directive}{CMD} is the last
\texttt{CMD} directive of the preceding configuration level.
\item \texttt{LOG} adds a file to be compared against an oracle in the
next \texttt{OPT} directive. Several files can be monitored from a single
\texttt{OPT} directive, through several \texttt{LOG} directives.
next \texttt{OPT} or \texttt{STDOPT} directive. Several files can be monitored from a single
\texttt{OPT}/\texttt{STDOPT} directive, through several \texttt{LOG} directives.
These files must be generated in the result
directory of the corresponding suite (and potentially alternative
configuration).
......
......@@ -785,13 +785,12 @@ let config_options =
let new_top =
List.map
(fun (cmd,opts, log, macros,_) ->
cmd, make_custom_opts opts s, log,
cmd, make_custom_opts opts s, log @ current.dc_default_log,
current.dc_macros, current.dc_timeout)
!current_default_cmds
in
{ current with dc_toplevels = new_top @ current.dc_toplevels;
dc_default_log = !current_default_log @
current.dc_default_log });
dc_default_log = !current_default_log });
"FILEREG",
(fun _ s current -> { current with dc_test_regexp = s });
......
......@@ -315,7 +315,10 @@ let dump () =
let fmt = Format.formatter_of_out_channel chan in
(match Metrics_base.get_file_type out with
| Metrics_base.Html -> dump_acsl_stats_html fmt
| Metrics_base.Text -> dump_acsl_stats fmt);
| Metrics_base.Text -> dump_acsl_stats fmt
| Metrics_base.Json ->
raise (Log.FeatureRequest ("Metrics", "JSON format for ACSL metrics"))
);
close_out chan
with Sys_error s ->
Metrics_parameters.abort "Cannot open file %s (%s)" out s
......
......@@ -248,6 +248,7 @@ let get_suffix filename =
type output_type =
| Html
| Text
| Json
;;
let get_file_type filename =
......@@ -255,6 +256,7 @@ let get_file_type filename =
match get_suffix filename with
| "html" | "htm" -> Html
| "txt" | "text" -> Text
| "json" -> Json
| s ->
Metrics_parameters.abort
"Unknown file extension %s. Cannot produce output.@." s
......@@ -285,6 +287,16 @@ let pretty_set fmt s =
s;
Format.fprintf fmt "@]"
let json_of_varinfo_map m =
let elems = VInfoMap.fold (fun f n acc ->
let calls = ("calls", `Int n) in
let address_taken = ("address_taken", `Bool f.vaddrof) in
let elem = `Assoc [(f.vname, `Assoc ([calls; address_taken]))] in
elem :: acc
) m []
in
`List (List.rev elems)
let pretty_extern_vars fmt s =
Pretty_utils.pp_iter ~pre:"@[" ~suf:"@]" ~sep:";@ "
VInfoSet.iter Printer.pp_varinfo fmt s
......@@ -312,6 +324,16 @@ let pretty_entry_points fmt fs =
Format.fprintf fmt "@[<hov 1>%a@]" print fs;
;;
let json_of_entry_points m =
`List
(List.rev
(VInfoMap.fold
(fun vi n acc ->
if is_entry_point vi n then `String vi.vname :: acc
else acc)
m [])
)
(* Utilities for CIL ASTs *)
let file_of_vinfodef fvinfo =
......
......@@ -108,6 +108,10 @@ val pretty_set : Format.formatter -> int VInfoMap.t -> unit
val pretty_extern_vars: Format.formatter -> VInfoSet.t -> unit
(** Build a JSON list with the varinfos in [m], each as a JSON object with
the varinfo name as key and additional attributes as values. *)
val json_of_varinfo_map : int VInfoMap.t -> Yojson.t
(** Handling entry points informations *)
val number_entry_points : int VInfoMap.t -> int
;;
......@@ -116,6 +120,8 @@ val pretty_entry_points :
Format.formatter -> int VInfoMap.t -> unit
;;
val json_of_entry_points : int VInfoMap.t -> Yojson.t
(** Get the filename where the definition of a varinfo occurs *)
val file_of_vinfodef: Cil_types.varinfo -> Datatype.Filepath.t;;
......@@ -133,6 +139,7 @@ val get_filename: Cabs.definition -> Datatype.Filepath.t;;
type output_type =
| Html
| Text
| Json
;;
(** get_file_type [extension] sets the output type according to [extension].
......
......@@ -662,6 +662,28 @@ let pp_funinfo fmt vis =
Metrics_base.pretty_entry_points vis#fundef_calls
;;
let json_of_funinfo vis =
let fundef =
("defined-functions", json_of_varinfo_map vis#fundef_calls)
in
let funspec =
("specified-only-functions", json_of_varinfo_map vis#funspec_calls)
in
let fundecl =
("undefined-functions", json_of_varinfo_map vis#fundecl_calls)
in
let extern_vars =
VInfoSet.fold (fun vi acc -> `String vi.vname :: acc)
vis#extern_global_vars []
in
let extern =
("extern-global-vars", `List (List.rev extern_vars))
in
let entry_points =
("entry-points", json_of_entry_points vis#fundef_calls)
in
`Assoc [fundef; funspec; fundecl; extern; entry_points]
let pp_with_funinfo fmt cil_visitor =
Format.fprintf fmt "@[<v 0>%a@ %a@]"
pp_funinfo cil_visitor
......@@ -721,6 +743,9 @@ let compute_on_cilast ~libc =
(match Metrics_base.get_file_type out_fname with
| Html -> dump_html fmt cil_visitor
| Text -> pp_with_funinfo fmt cil_visitor
| Json ->
let json = json_of_funinfo cil_visitor in
Yojson.pretty_print fmt json
);
close_out oc;
with Sys_error _ ->
......
......@@ -49,7 +49,8 @@ module OutputFile =
let option_name = "-metrics-output"
let arg_name = "filename"
let help = "print some metrics into the specified file; \
the output format is recognized through the extension."
the output format is recognized through the extension: \
.text/.txt for text, .html/.htm for HTML, or .json for JSON."
end)
module ValueCoverage =
......
/* run.config
STDOPT: #"-metrics-no-libc -metrics-eva-cover"
STDOPT: #"-metrics-libc -metrics-eva-cover"
LOG: libc.json
STDOPT: #"-metrics-libc -metrics-output @PTEST_DIR@/result/libc.json"
*/
#include <ctype.h>
#include <stdio.h> // defines external variables
......@@ -21,6 +23,8 @@ int g() { // called via fp
return isalpha(42);
}
int h() { return 0; }
int (*fp)() = g;
int getopt(int argc, char * const argv[],
......@@ -31,5 +35,6 @@ int getopt(int argc, char * const argv[],
int main() {
fp();
getopt(0, 0, 0);
h();
return isblank(0);
}
[kernel] Parsing tests/metrics/libc.c (with preprocessing)
[metrics] Defined functions (5)
[metrics] Defined functions (6)
=====================
bar (0 call); f (0 call); foo (0 call); g (address taken) (0 call);
main (0 call);
h (1 call); main (0 call);
Specified-only functions (0)
============================
......@@ -22,18 +22,18 @@
Global metrics
==============
Sloc = 12
Sloc = 15
Decision point = 0
Global variables = 1
If = 0
Loop = 0
Goto = 0
Assignment = 5
Exit point = 5
Function = 5
Function call = 5
Assignment = 6
Exit point = 6
Function = 6
Function call = 6
Pointer dereferencing = 1
Cyclomatic complexity = 5
Cyclomatic complexity = 6
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
......@@ -44,8 +44,8 @@
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
4 functions analyzed (out of 5): 80% coverage.
In these functions, 10 statements reached (out of 10): 100% coverage.
5 functions analyzed (out of 6): 83% coverage.
In these functions, 13 statements reached (out of 13): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
......@@ -58,15 +58,16 @@
----------------------------------------------------------------------------
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 4 (out of 5)
Semantically reached functions = 4
Syntactically reachable functions = 5 (out of 6)
Semantically reached functions = 5
Coverage estimation = 100.0%
[metrics] References to non-analyzed functions
------------------------------------
[metrics] Statements analyzed by Eva
--------------------------
10 stmts in analyzed functions, 10 stmts analyzed (100.0%)
13 stmts in analyzed functions, 13 stmts analyzed (100.0%)
bar: 2 stmts out of 2 (100.0%)
foo: 2 stmts out of 2 (100.0%)
g: 2 stmts out of 2 (100.0%)
main: 4 stmts out of 4 (100.0%)
h: 2 stmts out of 2 (100.0%)
main: 5 stmts out of 5 (100.0%)
[kernel] Parsing tests/metrics/libc.c (with preprocessing)
[metrics] Defined functions (6)
[metrics] Defined functions (7)
=====================
bar (1 call); f (0 call); foo (1 call); g (address taken) (0 call);
getopt (1 call); main (0 call);
getopt (1 call); h (1 call); main (0 call);
Specified-only functions (122)
==============================
......@@ -55,18 +55,18 @@
Global metrics
==============
Sloc = 17
Sloc = 20
Decision point = 0
Global variables = 17
If = 0
Loop = 0
Goto = 0
Assignment = 8
Exit point = 6
Function = 128
Function call = 7
Assignment = 9
Exit point = 7
Function = 129
Function call = 8
Pointer dereferencing = 1
Cyclomatic complexity = 6
Cyclomatic complexity = 7
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
......@@ -77,8 +77,8 @@
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
4 functions analyzed (out of 5): 80% coverage.
In these functions, 10 statements reached (out of 10): 100% coverage.
5 functions analyzed (out of 6): 83% coverage.
In these functions, 13 statements reached (out of 13): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
......@@ -91,16 +91,17 @@
----------------------------------------------------------------------------
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 7 (out of 128)
Semantically reached functions = 7
Syntactically reachable functions = 8 (out of 129)
Semantically reached functions = 8
Coverage estimation = 100.0%
[metrics] References to non-analyzed functions
------------------------------------
[metrics] Statements analyzed by Eva
--------------------------
15 stmts in analyzed functions, 15 stmts analyzed (100.0%)
18 stmts in analyzed functions, 18 stmts analyzed (100.0%)
bar: 2 stmts out of 2 (100.0%)
foo: 2 stmts out of 2 (100.0%)
g: 2 stmts out of 2 (100.0%)
getopt: 5 stmts out of 5 (100.0%)
main: 4 stmts out of 4 (100.0%)
h: 2 stmts out of 2 (100.0%)
main: 5 stmts out of 5 (100.0%)
[kernel] Parsing tests/metrics/libc.c (with preprocessing)
[kernel] Parsing tests/metrics/libc.c (with preprocessing)
{
"defined-functions": [
{ "bar": { "calls": 1, "address_taken": false } },
{ "f": { "calls": 0, "address_taken": false } },
{ "foo": { "calls": 1, "address_taken": false } },
{ "g": { "calls": 0, "address_taken": true } },
{ "getopt": { "calls": 1, "address_taken": false } },
{ "h": { "calls": 1, "address_taken": false } },
{ "main": { "calls": 0, "address_taken": false } }
],
"specified-only-functions": [
{ "_exit": { "calls": 0, "address_taken": false } },
{ "access": { "calls": 0, "address_taken": false } },
{ "chdir": { "calls": 0, "address_taken": false } },
{ "chown": { "calls": 0, "address_taken": false } },
{ "chroot": { "calls": 0, "address_taken": false } },
{ "clearerr": { "calls": 0, "address_taken": false } },
{ "clearerr_unlocked": { "calls": 0, "address_taken": false } },
{ "close": { "calls": 0, "address_taken": false } },
{ "dup": { "calls": 0, "address_taken": false } },
{ "dup2": { "calls": 0, "address_taken": false } },
{ "execl": { "calls": 0, "address_taken": false } },
{ "execle": { "calls": 0, "address_taken": false } },
{ "execlp": { "calls": 0, "address_taken": false } },
{ "execv": { "calls": 0, "address_taken": false } },
{ "execve": { "calls": 0, "address_taken": false } },
{ "execvp": { "calls": 0, "address_taken": false } },
{ "fclose": { "calls": 0, "address_taken": false } },
{ "fdopen": { "calls": 0, "address_taken": false } },
{ "feof": { "calls": 0, "address_taken": false } },
{ "feof_unlocked": { "calls": 0, "address_taken": false } },
{ "ferror": { "calls": 0, "address_taken": false } },
{ "ferror_unlocked": { "calls": 0, "address_taken": false } },
{ "fflush": { "calls": 0, "address_taken": false } },
{ "fgetc": { "calls": 0, "address_taken": false } },
{ "fgetpos": { "calls": 0, "address_taken": false } },
{ "fgets": { "calls": 0, "address_taken": false } },
{ "fileno": { "calls": 0, "address_taken": false } },
{ "fileno_unlocked": { "calls": 0, "address_taken": false } },
{ "flockfile": { "calls": 0, "address_taken": false } },
{ "fopen": { "calls": 0, "address_taken": false } },
{ "fork": { "calls": 0, "address_taken": false } },
{ "fputc": { "calls": 0, "address_taken": false } },
{ "fputs": { "calls": 0, "address_taken": false } },
{ "fread": { "calls": 0, "address_taken": false } },
{ "freopen": { "calls": 0, "address_taken": false } },
{ "fseek": { "calls": 0, "address_taken": false } },
{ "fseeko": { "calls": 0, "address_taken": false } },
{ "fsetpos": { "calls": 0, "address_taken": false } },
{ "ftell": { "calls": 0, "address_taken": false } },
{ "ftello": { "calls": 0, "address_taken": false } },
{ "ftrylockfile": { "calls": 0, "address_taken": false } },
{ "funlockfile": { "calls": 0, "address_taken": false } },
{ "fwrite": { "calls": 0, "address_taken": false } },
{ "getc": { "calls": 0, "address_taken": false } },
{ "getc_unlocked": { "calls": 0, "address_taken": false } },
{ "getchar": { "calls": 1, "address_taken": false } },
{ "getchar_unlocked": { "calls": 0, "address_taken": false } },
{ "getcwd": { "calls": 0, "address_taken": false } },
{ "getegid": { "calls": 0, "address_taken": false } },
{ "geteuid": { "calls": 0, "address_taken": false } },
{ "getgid": { "calls": 0, "address_taken": false } },
{ "gethostname": { "calls": 0, "address_taken": false } },
{ "getopt_long": { "calls": 0, "address_taken": false } },
{ "getopt_long_only": { "calls": 0, "address_taken": false } },
{ "getpgid": { "calls": 0, "address_taken": false } },
{ "getpgrp": { "calls": 0, "address_taken": false } },
{ "getpid": { "calls": 0, "address_taken": false } },
{ "getppid": { "calls": 0, "address_taken": false } },
{ "getresgid": { "calls": 0, "address_taken": false } },
{ "getresuid": { "calls": 0, "address_taken": false } },
{ "gets": { "calls": 0, "address_taken": false } },
{ "getsid": { "calls": 0, "address_taken": false } },
{ "getuid": { "calls": 0, "address_taken": false } },
{ "isalnum": { "calls": 0, "address_taken": false } },
{ "isalpha": { "calls": 1, "address_taken": false } },
{ "isascii": { "calls": 0, "address_taken": false } },
{ "isatty": { "calls": 0, "address_taken": false } },
{ "isblank": { "calls": 1, "address_taken": false } },
{ "iscntrl": { "calls": 0, "address_taken": false } },
{ "isdigit": { "calls": 0, "address_taken": false } },
{ "isgraph": { "calls": 0, "address_taken": false } },
{ "islower": { "calls": 0, "address_taken": false } },
{ "isprint": { "calls": 0, "address_taken": false } },
{ "ispunct": { "calls": 0, "address_taken": false } },
{ "isspace": { "calls": 0, "address_taken": false } },
{ "isupper": { "calls": 0, "address_taken": false } },
{ "isxdigit": { "calls": 0, "address_taken": false } },
{ "lseek": { "calls": 0, "address_taken": false } },
{ "pathconf": { "calls": 0, "address_taken": false } },
{ "pclose": { "calls": 0, "address_taken": false } },
{ "perror": { "calls": 0, "address_taken": false } },
{ "pipe": { "calls": 0, "address_taken": false } },
{ "popen": { "calls": 0, "address_taken": false } },
{ "putc": { "calls": 0, "address_taken": false } },
{ "putc_unlocked": { "calls": 0, "address_taken": false } },
{ "putchar": { "calls": 0, "address_taken": false } },
{ "putchar_unlocked": { "calls": 0, "address_taken": false } },
{ "puts": { "calls": 0, "address_taken": false } },
{ "read": { "calls": 0, "address_taken": false } },
{ "remove": { "calls": 0, "address_taken": false } },
{ "rename": { "calls": 0, "address_taken": false } },
{ "rewind": { "calls": 0, "address_taken": false } },
{ "setbuf": { "calls": 0, "address_taken": false } },
{ "setegid": { "calls": 0, "address_taken": false } },
{ "seteuid": { "calls": 0, "address_taken": false } },
{ "setgid": { "calls": 0, "address_taken": false } },
{ "sethostname": { "calls": 0, "address_taken": false } },
{ "setpgid": { "calls": 0, "address_taken": false } },
{ "setregid": { "calls": 0, "address_taken": false } },
{ "setresgid": { "calls": 0, "address_taken": false } },
{ "setresuid": { "calls": 0, "address_taken": false } },
{ "setreuid": { "calls": 0, "address_taken": false } },
{ "setsid": { "calls": 0, "address_taken": false } },
{ "setuid": { "calls": 0, "address_taken": false } },
{ "setvbuf": { "calls": 0, "address_taken": false } },
{ "sync": { "calls": 0, "address_taken": false } },
{ "sysconf": { "calls": 0, "address_taken": false } },
{ "tmpfile": { "calls": 0, "address_taken": false } },
{ "tmpnam": { "calls": 0, "address_taken": false } },
{ "tolower": { "calls": 0, "address_taken": false } },
{ "toupper": { "calls": 0, "address_taken": false } },
{ "ttyname": { "calls": 0, "address_taken": false } },
{ "ungetc": { "calls": 0, "address_taken": false } },
{ "unlink": { "calls": 0, "address_taken": false } },
{ "usleep": { "calls": 0, "address_taken": false } },
{ "vfprintf": { "calls": 0, "address_taken": false } },
{ "vfscanf": { "calls": 0, "address_taken": false } },
{ "vprintf": { "calls": 0, "address_taken": false } },
{ "vscanf": { "calls": 0, "address_taken": false } },
{ "vsnprintf": { "calls": 0, "address_taken": false } },
{ "vsprintf": { "calls": 0, "address_taken": false } },
{ "write": { "calls": 0, "address_taken": false } }
],
"undefined-functions": [],
"extern-global-vars": [
"Frama_C_entropy_source", "__fc_errno", "__fc_hostname", "__fc_stdin",
"__fc_stdout", "__fc_ttyname", "optarg", "opterr", "optind", "optopt"
],
"entry-points": [ "f", "main" ]
}
\ No newline at end of file
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