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
668834f2
Commit
668834f2
authored
1 year ago
by
Thibault Martin
Committed by
Virgile Prevosto
1 year ago
Browse files
Options
Downloads
Patches
Plain Diff
Use new Current_loc API in scope/from/loop_analysis
parent
535d2141
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
src/plugins/from/from_compute.ml
+5
-9
5 additions, 9 deletions
src/plugins/from/from_compute.ml
src/plugins/loop_analysis/loop_analysis.ml
+2
-1
2 additions, 1 deletion
src/plugins/loop_analysis/loop_analysis.ml
src/plugins/scope/datascope.ml
+2
-1
2 additions, 1 deletion
src/plugins/scope/datascope.ml
with
9 additions
and
11 deletions
src/plugins/from/from_compute.ml
+
5
−
9
View file @
668834f2
...
...
@@ -200,15 +200,11 @@ struct
is redundant with the work done by Value -- hence the use of [\nothing].*)
let
bind_locals
m
b
=
let
aux_local
acc
vi
=
Current_loc
.
set
vi
.
vdecl
;
(* Consider that local are initialized to a constant value *)
From_memory
.
bind_var
vi
Eva
.
Deps
.
bottom
acc
Current_loc
.
with_loc
vi
.
vdecl
(
From_memory
.
bind_var
vi
Eva
.
Deps
.
bottom
)
acc
in
let
loc
=
Current_loc
.
get
()
in
let
r
=
List
.
fold_left
aux_local
m
b
.
blocals
in
Current_loc
.
set
loc
;
r
List
.
fold_left
aux_local
m
b
.
blocals
let
unbind_locals
m
b
=
let
aux_local
acc
vi
=
...
...
@@ -631,7 +627,8 @@ struct
compute_using_prototype_for_state
state
kf
assigns
let
compute_and_return
kf
=
let
call_site_loc
=
Current_loc
.
get
()
in
let
open
Current_loc
.
Operators
in
let
<>
UpdatedCurrentLoc
=
Current_loc
.
get
()
in
From_parameters
.
feedback
"Computing for function %a%s"
Kernel_function
.
pretty
kf
...
...
@@ -651,7 +648,6 @@ struct
From_parameters
.
feedback
"Done for function %a"
Kernel_function
.
pretty
kf
;
Async
.
yield
()
;
Current_loc
.
set
call_site_loc
;
result
let
compute
kf
=
...
...
This diff is collapsed.
Click to expand it.
src/plugins/loop_analysis/loop_analysis.ml
+
2
−
1
View file @
668834f2
...
...
@@ -361,7 +361,8 @@ module Store(* (B:sig *)
end
let
mu
(
f
:
(
t
->
t
))
(
value
,
conds
,
stmt
)
=
Current_loc
.
set
(
Cil_datatype
.
Stmt
.
loc
stmt
);
let
open
Current_loc
.
Operators
in
let
<>
UpdatedCurrentLoc
=
Cil_datatype
.
Stmt
.
loc
stmt
in
let
(
result
,
final_conds
,_
)
=
f
(
init
stmt
)
in
(* Induction variables is a map from each Varinfo to its increment. *)
...
...
This diff is collapsed.
Click to expand it.
src/plugins/scope/datascope.ml
+
2
−
1
View file @
668834f2
...
...
@@ -126,10 +126,11 @@ let register_modified_zones lmap stmt =
* @raise Kernel_function.No_Definition if [kf] has no definition
*)
let
compute
kf
=
let
open
Current_loc
.
Operators
in
R
.
debug
~
level
:
1
"computing for function %a"
Kernel_function
.
pretty
kf
;
let
f
=
Kernel_function
.
get_definition
kf
in
let
do_stmt
lmap
s
=
Current_loc
.
set
(
Cil_datatype
.
Stmt
.
loc
s
);
let
<>
UpdatedCurrentLoc
=
Cil_datatype
.
Stmt
.
loc
s
in
if
Eva
.
Results
.
is_reachable
s
then
register_modified_zones
lmap
s
else
lmap
...
...
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