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
4d1dfd7e
Commit
4d1dfd7e
authored
5 years ago
by
Valentin Perrelle
Committed by
David Bühler
4 years ago
Browse files
Options
Downloads
Patches
Plain Diff
[Dive] Send information about updated nodes
parent
0ffedd6b
No related branches found
No related tags found
No related merge requests found
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
src/plugins/dive/build.ml
+11
-4
11 additions, 4 deletions
src/plugins/dive/build.ml
src/plugins/dive/imprecision_graph.ml
+11
-11
11 additions, 11 deletions
src/plugins/dive/imprecision_graph.ml
src/plugins/dive/imprecision_graph.mli
+7
-1
7 additions, 1 deletion
src/plugins/dive/imprecision_graph.mli
with
29 additions
and
16 deletions
src/plugins/dive/build.ml
+
11
−
4
View file @
4d1dfd7e
...
...
@@ -198,13 +198,19 @@ type t = {
let
get_node
context
node_key
=
VertexTable
.
find
context
.
vertex_table
node_key
let
update_node
context
node
=
if
not
(
List
.
exists
(
Graph
.
Node
.
equal
node
)
context
.
graph_diff
.
added_nodes
)
then
context
.
graph_diff
<-
{
context
.
graph_diff
with
added_nodes
=
node
::
context
.
graph_diff
.
added_nodes
}
let
add_node
context
~
node_kind
~
node_locality
=
let
node
=
Graph
.
create_node
context
.
graph
~
node_kind
~
node_locality
in
VertexTable
.
add
context
.
vertex_table
node
.
node_key
node
;
context
.
graph_diff
<-
{
context
.
graph_diff
with
added_nodes
=
node
::
context
.
graph_diff
.
added_nodes
};
update_node
context
node
;
node
let
_remove_node
context
node
=
...
...
@@ -438,6 +444,7 @@ let build_node_deps context node =
Graph
.
create_dependency
~
allow_folding
context
.
graph
dst
kind
node
in
update_node
context
node
;
let
callstack
=
node
.
node_locality
.
loc_callstack
in
match
node
.
node_kind
with
|
Scalar
(
vi
,_
typ
,
offset
)
->
...
...
This diff is collapsed.
Click to expand it.
src/plugins/dive/imprecision_graph.ml
+
11
−
11
View file @
4d1dfd7e
...
...
@@ -22,7 +22,7 @@
open
Graph_types
module
Vertex
=
module
Node
=
struct
type
t
=
node
let
compare
v1
v2
=
v1
.
node_key
-
v2
.
node_key
...
...
@@ -30,12 +30,12 @@ struct
let
equal
v1
v2
=
v1
.
node_key
=
v2
.
node_key
end
module
Edge
=
module
Dependency
=
struct
type
t
=
dependency
let
compare
e1
e2
=
e1
.
dependency_key
-
e2
.
dependency_key
let
_
hash
e
=
e
.
dependency_key
let
_
equal
e1
e2
=
e1
.
dependency_key
=
e2
.
dependency_key
let
hash
e
=
e
.
dependency_key
let
equal
e1
e2
=
e1
.
dependency_key
=
e2
.
dependency_key
let
default
=
{
dependency_key
=
-
1
;
dependency_kind
=
Data
;
...
...
@@ -43,22 +43,22 @@ struct
}
end
module
G
=
Graph
.
Imperative
.
Digraph
.
ConcreteBidirectionalLabeled
(
Vertex
)
(
Edge
)
module
G
=
Graph
.
Imperative
.
Digraph
.
ConcreteBidirectionalLabeled
(
Node
)
(
Dependency
)
include
G
let
next_node_key
=
ref
0
let
next_dependency_key
=
ref
0
let
next_key
=
ref
0
let
create_node
?
node_values
~
node_kind
~
node_locality
g
=
let
node
=
{
node_key
=
!
next_
node_
key
;
node_key
=
!
next_key
;
node_kind
;
node_locality
;
node_values
;
node_deps_computed
=
false
;
}
in
incr
next_
node_
key
;
incr
next_key
;
add_vertex
g
node
;
node
...
...
@@ -104,12 +104,12 @@ let create_dependency ~allow_folding g v1 dependency_kind v2 =
e
.
dependency_multiple
<-
true
|
None
->
let
e
=
{
dependency_key
=
!
next_
dependency_
key
;
dependency_key
=
!
next_key
;
dependency_kind
;
dependency_multiple
=
false
;
}
in
incr
next_
dependency_
key
;
incr
next_key
;
add_edge_e
g
(
v1
,
e
,
v2
)
...
...
This diff is collapsed.
Click to expand it.
src/plugins/dive/imprecision_graph.mli
+
7
−
1
View file @
4d1dfd7e
...
...
@@ -22,7 +22,13 @@
open
Graph_types
include
Graph
.
Sig
.
G
with
type
V
.
t
=
node
include
Graph
.
Sig
.
G
with
type
V
.
t
=
node
and
type
E
.
t
=
node
*
dependency
*
node
module
Node
:
Graph
.
Sig
.
COMPARABLE
with
type
t
=
node
module
Dependency
:
Graph
.
Sig
.
COMPARABLE
with
type
t
=
dependency
val
create
:
?
size
:
int
->
unit
->
t
...
...
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