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
bf0c0060
Commit
bf0c0060
authored
6 years ago
by
David Bühler
Committed by
Andre Maroneze
6 years ago
Browse files
Options
Downloads
Patches
Plain Diff
[From] Avoids folding implicit zero-initializers of large arrays.
Fixes a performance issue.
parent
ff4cd3b7
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/from/from_compute.ml
+15
-2
15 additions, 2 deletions
src/plugins/from/from_compute.ml
with
15 additions
and
2 deletions
src/plugins/from/from_compute.ml
+
15
−
2
View file @
bf0c0060
...
@@ -463,7 +463,6 @@ struct
...
@@ -463,7 +463,6 @@ struct
let
init
=
Cil
.
is_mutable_or_initialized
lv
in
let
init
=
Cil
.
is_mutable_or_initialized
lv
in
transfer_assign
stmt
~
init
lv
comp_vars
state
transfer_assign
stmt
~
init
lv
comp_vars
state
|
Local_init
(
v
,
AssignInit
i
,
_
)
->
|
Local_init
(
v
,
AssignInit
i
,
_
)
->
let
implicit
=
true
in
let
rec
aux
lv
i
acc
=
let
rec
aux
lv
i
acc
=
let
doinit
o
i
_
state
=
aux
(
Cil
.
addOffsetLval
o
lv
)
i
state
in
let
doinit
o
i
_
state
=
aux
(
Cil
.
addOffsetLval
o
lv
)
i
state
in
match
i
with
match
i
with
...
@@ -471,7 +470,21 @@ struct
...
@@ -471,7 +470,21 @@ struct
let
comp_vars
=
find
stmt
acc
.
deps_table
e
in
let
comp_vars
=
find
stmt
acc
.
deps_table
e
in
transfer_assign
stmt
~
init
:
true
lv
comp_vars
acc
transfer_assign
stmt
~
init
:
true
lv
comp_vars
acc
|
CompoundInit
(
ct
,
initl
)
->
|
CompoundInit
(
ct
,
initl
)
->
Cil
.
foldLeftCompound
~
implicit
~
doinit
~
ct
~
initl
~
acc
(* To avoid a performance issue, do not fold implicit initializers
of scalar or large arrays. We still use implicit initializers
for small struct arrays, as this may be more precise in case of
padding bits. The 100 limit is arbitrary. *)
let
implicit
=
not
(
Cil
.
isArrayType
ct
&&
(
Cil
.
isArithmeticOrPointerType
(
Cil
.
typeOf_array_elem
ct
)
||
Ast_info
.
array_size
ct
>
(
Integer
.
of_int
100
)))
in
let
r
=
Cil
.
foldLeftCompound
~
implicit
~
doinit
~
ct
~
initl
~
acc
in
if
implicit
then
r
else
(* If implicit zero-initializers have been skipped, also mark
the entire array as initialized from no dependency (nothing
is read by the implicit zero-initializers). *)
transfer_assign
stmt
~
init
:
true
lv
Function_Froms
.
Deps
.
bottom
r
in
in
aux
(
Cil
.
var
v
)
i
state
aux
(
Cil
.
var
v
)
i
state
|
Call
(
lvaloption
,
funcexp
,
argl
,
loc
)
->
|
Call
(
lvaloption
,
funcexp
,
argl
,
loc
)
->
...
...
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