Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
f70cdc4a
Commit
f70cdc4a
authored
Oct 13, 2020
by
Andre Maroneze
💬
Browse files
[Metrics] add (partial) support for JSON output
parent
0aab40cd
Changes
8
Hide whitespace changes
Inline
Side-by-side
src/plugins/metrics/metrics_acsl.ml
View file @
f70cdc4a
...
...
@@ -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
...
...
src/plugins/metrics/metrics_base.ml
View file @
f70cdc4a
...
...
@@ -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
=
...
...
src/plugins/metrics/metrics_base.mli
View file @
f70cdc4a
...
...
@@ -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].
...
...
src/plugins/metrics/metrics_cilast.ml
View file @
f70cdc4a
...
...
@@ -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
_
->
...
...
src/plugins/metrics/metrics_parameters.ml
View file @
f70cdc4a
...
...
@@ -49,7 +49,9 @@ 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. \
If the filename is only the extension (txt, html, json), \
print to stdout but in the specified format."
end
)
module
ValueCoverage
=
...
...
tests/metrics/libc.c
View file @
f70cdc4a
/* run.config
STDOPT: #"-metrics-no-libc -metrics-eva-cover"
STDOPT: #"-metrics-libc -metrics-eva-cover"
STDOPT: #"-metrics-libc -metrics-output @PTEST_DIR@/oracle/libc.json"
LOG: @PTEST_DIR@/oracle/libc.json
*/
#include <ctype.h>
#include <stdio.h> // defines external variables
...
...
tests/metrics/oracle/libc.2.res.oracle
0 → 100644
View file @
f70cdc4a
[kernel] Parsing tests/metrics/libc.c (with preprocessing)
tests/metrics/oracle/libc.json
0 → 100644
View file @
f70cdc4a
{
"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
}
},
{
"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
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment