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
d31f2b65
Commit
d31f2b65
authored
2 years ago
by
David Bühler
Browse files
Options
Downloads
Patches
Plain Diff
[Dive] Minor code factorization in build_node_writes.
parent
ad68ddf1
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/dive/build.ml
+17
-16
17 additions, 16 deletions
src/plugins/dive/build.ml
with
17 additions
and
16 deletions
src/plugins/dive/build.ml
+
17
−
16
View file @
d31f2b65
...
...
@@ -327,8 +327,7 @@ let build_node_writes context node =
Seq
.
append
args_seq
(
Seq
.
flat_map
add_deps
(
List
.
to_seq
writes
))
and
build_alarm_deps
callstack
stmt
alarm
:
deps_builder
=
List
.
to_seq
(
EnumLvals
.
in_alarm
alarm
)
|>
Seq
.
flat_map
(
build_lval_deps
callstack
stmt
Data
)
build_lvals_deps
callstack
stmt
Data
(
EnumLvals
.
in_alarm
alarm
)
and
build_instr_deps
callstack
stmt
instr
:
deps_builder
=
(* Add dependencies found in the instruction *)
...
...
@@ -344,17 +343,12 @@ let build_node_writes context node =
Cil
.
treat_constructor_as_func
as_func
dest
f
args
k
loc
|
Local_init
(
vi
,
AssignInit
init
,
_
)
->
let
lvals
=
EnumLvals
.
in_init
vi
init
in
if
lvals
<>
[]
then
List
.
to_seq
lvals
|>
Seq
.
flat_map
(
build_lval_deps
callstack
stmt
Data
)
else
begin
match
init
with
|
CompoundInit
_
->
Seq
.
empty
(* Do not generate nodes for Compounds for now *)
|
SingleInit
exp
->
let
kinstr
=
Kstmt
stmt
in
let
dst
=
build_const
context
callstack
exp
in
Seq
.
return
(
Graph
.
create_dependency
graph
kinstr
dst
Data
node
)
end
let
exp
=
match
init
with
|
CompoundInit
_
->
None
(* Do not generate nodes for Compounds for now *)
|
SingleInit
exp
->
Some
exp
in
build_lvals_deps
callstack
stmt
Data
?
exp
lvals
|
Asm
_
|
Skip
_
|
Code_annot
_
->
Seq
.
empty
(* Cases not returned by Studia *)
and
build_arg_deps
callstack
:
deps_builder
*
stmt
list
=
...
...
@@ -414,19 +408,26 @@ let build_node_writes context node =
and
build_exp_deps
callstack
stmt
kind
exp
:
deps_builder
=
let
lvals
=
EnumLvals
.
in_exp
exp
in
build_lvals_deps
callstack
stmt
kind
~
exp
lvals
and
build_lvals_deps
callstack
stmt
kind
?
exp
lvals
:
deps_builder
=
if
lvals
<>
[]
then
List
.
to_seq
lvals
|>
Seq
.
flat_map
(
build_lval_deps
callstack
stmt
kind
)
else
let
kinstr
=
Kstmt
stmt
in
let
dst
=
build_const
context
callstack
exp
in
Seq
.
return
(
Graph
.
create_dependency
graph
kinstr
dst
kind
node
)
Option
.
fold
exp
~
none
:
Seq
.
empty
~
some
:
(
build_const_deps
callstack
stmt
kind
)
and
build_lval_deps
callstack
stmt
kind
lval
:
deps_builder
=
let
kinstr
=
Kstmt
stmt
in
let
dst
=
build_lval
context
callstack
kinstr
lval
in
Seq
.
return
(
Graph
.
create_dependency
graph
kinstr
dst
kind
node
)
and
build_const_deps
callstack
stmt
kind
exp
:
deps_builder
=
let
kinstr
=
Kstmt
stmt
in
let
dst
=
build_const
context
callstack
exp
in
Seq
.
return
(
Graph
.
create_dependency
graph
kinstr
dst
kind
node
)
and
build_scattered_deps
callstack
kinstr
lval
:
deps_builder
=
let
add_cell
node_kind
=
let
node'
=
add_or_update_node
context
callstack
node_kind
in
...
...
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