Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
f055ab00
Commit
f055ab00
authored
2 years ago
by
David Bühler
Browse files
Options
Downloads
Patches
Plain Diff
[Eva] Statistics file: adds columns for function and statement location.
parent
5bdee261
No related branches found
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
src/plugins/eva/utils/statistics.ml
+61
-42
61 additions, 42 deletions
src/plugins/eva/utils/statistics.ml
tests/value/oracle/statistics.stats
+7
-7
7 additions, 7 deletions
tests/value/oracle/statistics.stats
with
68 additions
and
49 deletions
src/plugins/eva/utils/statistics.ml
+
61
−
42
View file @
f055ab00
...
@@ -91,46 +91,61 @@ let register_statement_stat name =
...
@@ -91,46 +91,61 @@ let register_statement_stat name =
type
key
=
Key
:
'
a
t
*
'
a
->
key
type
key
=
Key
:
'
a
t
*
'
a
->
key
module
Key
=
Datatype
.
Make_with_collections
(
module
Key_Datatype
=
struct
struct
include
Datatype
.
Serializable_undefined
include
Datatype
.
Serializable_undefined
type
t
=
key
type
t
=
key
let
name
=
"Statistics.Key"
let
name
=
"Statistics.Key"
let
rehash
(
Key
(
s
,
x
))
=
let
rehash
(
Key
(
s
,
x
))
=
(
Key
(
register
s
.
name
s
.
kind
,
x
))
(
Key
(
register
s
.
name
s
.
kind
,
x
))
let
reprs
=
[
Key
({
id
=
0
;
name
=
"dummy"
;
kind
=
Global
}
,
()
)]
let
reprs
=
[
Key
({
id
=
0
;
name
=
"dummy"
;
kind
=
Global
}
,
()
)]
let
equal
=
Datatype
.
from_compare
let
equal
=
Datatype
.
from_compare
let
compare
(
Key
(
s1
,
x1
))
(
Key
(
s2
,
x2
))
=
let
compare
(
Key
(
s1
,
x1
))
(
Key
(
s2
,
x2
))
=
let
c
=
s1
.
id
-
s2
.
id
in
let
c
=
s1
.
id
-
s2
.
id
in
if
c
<>
0
then
c
else
if
c
<>
0
then
c
else
match
s1
.
kind
,
s2
.
kind
with
match
s1
.
kind
,
s2
.
kind
with
|
Global
,
Global
->
0
|
Global
,
Global
->
0
|
Function
,
Function
->
Kernel_function
.
compare
x1
x2
|
Function
,
Function
->
Kernel_function
.
compare
x1
x2
|
Statement
,
Statement
->
Cil_datatype
.
Stmt
.
compare
x1
x2
|
Statement
,
Statement
->
Cil_datatype
.
Stmt
.
compare
x1
x2
|
Global
,
(
Function
|
Statement
)
->
-
1
|
Global
,
(
Function
|
Statement
)
->
-
1
|
(
Function
|
Statement
)
,
Global
->
1
|
(
Function
|
Statement
)
,
Global
->
1
|
Function
,
Statement
->
-
1
|
Function
,
Statement
->
-
1
|
Statement
,
Function
->
1
|
Statement
,
Function
->
1
let
hash
(
Key
(
s
,
x
))
=
let
hash
(
Key
(
s
,
x
))
=
let
h
=
match
s
.
kind
with
let
h
=
match
s
.
kind
with
|
Global
->
0
|
Global
->
0
|
Function
->
Kernel_function
.
hash
x
|
Function
->
Kernel_function
.
hash
x
|
Statement
->
Cil_datatype
.
Stmt
.
hash
x
|
Statement
->
Cil_datatype
.
Stmt
.
hash
x
in
in
Hashtbl
.
hash
(
s
.
id
,
h
)
Hashtbl
.
hash
(
s
.
id
,
h
)
let
copy
k
=
k
let
copy
k
=
k
let
pretty
fmt
(
Key
(
s
,
x
))
=
let
pretty
fmt
(
Key
(
s
,
x
))
=
match
s
.
kind
with
match
s
.
kind
with
|
Global
->
|
Global
->
Format
.
fprintf
fmt
"%s"
s
.
name
Format
.
fprintf
fmt
"%s"
s
.
name
|
Function
->
|
Function
->
Format
.
fprintf
fmt
"%s:%a"
s
.
name
Kernel_function
.
pretty
x
Format
.
fprintf
fmt
"%s:%a"
s
.
name
Kernel_function
.
pretty
x
|
Statement
->
|
Statement
->
let
loc
=
Cil_datatype
.
Stmt
.
loc
x
in
let
loc
=
Cil_datatype
.
Stmt
.
loc
x
in
Format
.
fprintf
fmt
"%s:%a"
s
.
name
Cil_datatype
.
Location
.
pretty
loc
Format
.
fprintf
fmt
"%s:%a"
s
.
name
Cil_datatype
.
Location
.
pretty
loc
end
end
)
module
Key
=
struct
include
Datatype
.
Make_with_collections
(
Key_Datatype
)
let
name
(
Key
(
s
,
_x
))
=
s
.
name
let
pretty_kf
fmt
(
Key
(
s
,
x
))
=
match
s
.
kind
with
|
Global
->
()
|
Function
->
Kernel_function
.
pretty
fmt
x
|
Statement
->
Kernel_function
.(
pretty
fmt
(
find_englobing_kf
x
))
let
pretty_stmt
fmt
(
Key
(
s
,
x
))
=
match
s
.
kind
with
|
Global
|
Function
->
()
|
Statement
->
Cil_datatype
.
Location
.
pretty
fmt
(
Cil_datatype
.
Stmt
.
loc
x
)
end
(* --- Projectified state --- *)
(* --- Projectified state --- *)
...
@@ -174,8 +189,12 @@ let export_as_list () =
...
@@ -174,8 +189,12 @@ let export_as_list () =
let
export_as_csv_to_channel
out_channel
=
let
export_as_csv_to_channel
out_channel
=
let
fmt
=
Format
.
formatter_of_out_channel
out_channel
in
let
fmt
=
Format
.
formatter_of_out_channel
out_channel
in
let
l
=
export_as_list
()
in
let
l
=
export_as_list
()
in
let
pp_stat
fmt
(
k
,
v
)
=
let
pp_stat
fmt
(
key
,
value
)
=
Format
.
fprintf
fmt
"%a
\t
%d
\n
"
Key
.
pretty
k
v
Format
.
fprintf
fmt
"%s
\t
%a
\t
%a
\t
%d
\n
"
(
Key
.
name
key
)
Key
.
pretty_kf
key
Key
.
pretty_stmt
key
value
in
in
List
.
iter
(
pp_stat
fmt
)
l
List
.
iter
(
pp_stat
fmt
)
l
...
...
This diff is collapsed.
Click to expand it.
tests/value/oracle/statistics.stats
+
7
−
7
View file @
f055ab00
memexec-hits
:g
3
memexec-hits
g
3
memexec-misses
:g
5
memexec-misses
g
5
memexec-misses
:f
2
memexec-misses
f
2
memexec-misses
:
main 1
memexec-misses
main
1
partitioning-index-misses 57
partitioning-index-misses
57
max-widenings
:
statistics.i:12 1
max-widenings
f
statistics.i:12 1
iterations
:
statistics.i:12 8
iterations
f
statistics.i:12 8
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment