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
01a129da
Commit
01a129da
authored
5 years ago
by
David Bühler
Browse files
Options
Downloads
Patches
Plain Diff
[Eva] Minor optimization when building the abstractions for an analysis.
Do not lift the abstract locations if it is not needed.
parent
031b40c6
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/value/engine/abstractions.ml
+29
-13
29 additions, 13 deletions
src/plugins/value/engine/abstractions.ml
with
29 additions
and
13 deletions
src/plugins/value/engine/abstractions.ml
+
29
−
13
View file @
01a129da
...
@@ -125,6 +125,11 @@ module Leaf_Value (V: Abstract_value.Leaf) = struct
...
@@ -125,6 +125,11 @@ module Leaf_Value (V: Abstract_value.Leaf) = struct
let
structure
=
Abstract
.
Value
.
Leaf
(
V
.
key
,
(
module
V
))
let
structure
=
Abstract
.
Value
.
Leaf
(
V
.
key
,
(
module
V
))
end
end
module
Leaf_Location
(
Loc
:
Abstract_location
.
Leaf
)
=
struct
include
Loc
let
structure
=
Abstract
.
Location
.
Leaf
(
Loc
.
key
,
(
module
Loc
))
end
module
Leaf_Domain
(
D
:
Abstract_domain
.
Leaf
)
=
struct
module
Leaf_Domain
(
D
:
Abstract_domain
.
Leaf
)
=
struct
include
D
include
D
let
structure
=
Abstract
.
Domain
.
Leaf
(
D
.
key
,
(
module
D
))
let
structure
=
Abstract
.
Domain
.
Leaf
(
D
.
key
,
(
module
D
))
...
@@ -219,8 +224,10 @@ end
...
@@ -219,8 +224,10 @@ end
(* --- Building domain abstractions ----------------------------------------- *)
(* --- Building domain abstractions ----------------------------------------- *)
module
type
internal_loc
=
Abstract
.
Location
.
Internal
with
type
location
=
precise_loc
module
type
internal_domain
=
module
type
internal_domain
=
Abstract
.
Domain
.
Internal
with
type
location
=
Precise_locs
.
precise_loc
ation
Abstract
.
Domain
.
Internal
with
type
location
=
precise_loc
let
eq_value
:
let
eq_value
:
type
a
b
.
a
Abstract
.
Value
.
structure
->
b
value
->
(
a
,
b
)
Structure
.
eq
option
type
a
b
.
a
Abstract
.
Value
.
structure
->
b
value
->
(
a
,
b
)
Structure
.
eq
option
...
@@ -379,25 +386,34 @@ module Open (Acc: Acc) : S = struct
...
@@ -379,25 +386,34 @@ module Open (Acc: Acc) : S = struct
end
end
end
end
module
Unit_Acc
(
Value
:
Abstract
.
Value
.
External
)
:
Acc
=
struct
module
CVal
=
Leaf_Value
(
Main_values
.
CVal
)
module
Struct
=
struct
type
v
=
Cvalue
.
V
.
t
let
unit_acc
(
module
Value
:
Abstract
.
Value
.
External
)
=
let
s
=
Single
(
module
Main_values
.
CVal
)
let
loc
:
(
module
internal_loc
with
type
value
=
Value
.
t
)
=
end
match
Abstract
.
Value
.
eq_structure
Value
.
structure
CVal
.
structure
with
module
Conv
=
Internal_Value
.
Convert
(
Value
)
(
Struct
)
|
Some
Structure
.
Eq
->
(
module
Leaf_Location
(
Main_locations
.
PLoc
))
module
Val
=
Value
|
_
->
module
Loc
=
Location_lift
.
Make
(
Main_locations
.
PLoc
)
(
Conv
)
let
module
Struct
=
struct
module
Dom
=
Unit_domain
.
Make
(
Value
)
(
Loc
)
type
v
=
Cvalue
.
V
.
t
end
let
s
=
Single
(
module
Main_values
.
CVal
)
end
in
let
module
Conv
=
Internal_Value
.
Convert
(
Value
)
(
Struct
)
in
(
module
Location_lift
.
Make
(
Main_locations
.
PLoc
)
(
Conv
))
in
(
module
struct
module
Val
=
Value
module
Loc
=
(
val
loc
)
module
Dom
=
Unit_domain
.
Make
(
Val
)
(
Loc
)
end
:
Acc
)
let
build_abstractions
config
=
let
build_abstractions
config
=
let
initial_value
:
(
module
Abstract
.
Value
.
Internal
)
=
let
initial_value
:
(
module
Abstract
.
Value
.
Internal
)
=
if
Config
.
mem
Config
.
bitwise
config
if
Config
.
mem
Config
.
bitwise
config
then
(
module
Offsm_value
.
CvalueOffsm
)
then
(
module
Offsm_value
.
CvalueOffsm
)
else
(
module
Leaf_Value
(
Main_values
.
CVal
)
)
else
(
module
CVal
)
in
in
let
value
=
Internal_Value
.
build_values
config
initial_value
in
let
value
=
Internal_Value
.
build_values
config
initial_value
in
let
acc
=
(
module
U
nit_
A
cc
(
val
value
)
:
Acc
)
in
let
acc
=
u
nit_
a
cc
value
in
build_domain
config
acc
build_domain
config
acc
let
configure
=
Config
.
configure
let
configure
=
Config
.
configure
...
...
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