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
00ac995c
Commit
00ac995c
authored
2 years ago
by
David Bühler
Browse files
Options
Downloads
Patches
Plain Diff
[from] Uses Eva.Cvalue_callbacks hooks instead of Db.Value.
parent
44c04724
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/callwise.ml
+11
-20
11 additions, 20 deletions
src/plugins/from/callwise.ml
with
11 additions
and
20 deletions
src/plugins/from/callwise.ml
+
11
−
20
View file @
00ac995c
...
...
@@ -64,9 +64,9 @@ let record_callwise_dependencies_in_db call_site froms =
Tbl
.
replace
call_site
(
Function_Froms
.
join
previous
froms
)
with
Not_found
->
Tbl
.
add
call_site
froms
let
call_for_individual_froms
(
call_type
,
value_initial_state
,
call_stack
)
=
let
call_for_individual_froms
callstack
_kf
call_type
value_initial_state
=
if
From_parameters
.
ForceCallDeps
.
get
()
then
begin
let
current_function
,
call_site
=
List
.
hd
call
_
stack
in
let
current_function
,
call_site
=
List
.
hd
callstack
in
let
register_from
froms
=
record_callwise_dependencies_in_db
call_site
froms
;
match
!
call_froms_stack
with
...
...
@@ -151,15 +151,13 @@ let compute_call_from_value_states current_function states =
Callwise_Froms
.
compute_and_return
current_function
let
record_for_individual_froms
(
call
_
stack
,
value_res
)
=
let
record_for_individual_froms
callstack
cur_kf
value_res
=
if
From_parameters
.
ForceCallDeps
.
get
()
then
begin
let
froms
=
match
value_res
with
|
Value_types
.
Normal
(
states
,
_after_states
)
|
Value_types
.
NormalStore
((
states
,
_after_states
)
,
_
)
->
let
cur_kf
,
_
=
List
.
hd
call_stack
in
|
Eva
.
Cvalue_callbacks
.
Store
({
before_stmts
}
,
memexec_counter
)
->
let
froms
=
if
Eva
.
Analysis
.
save_results
cur_kf
then
compute_call_from_value_states
cur_kf
(
Lazy
.
force
state
s
)
then
compute_call_from_value_states
cur_kf
(
Lazy
.
force
before_stmt
s
)
else
Function_Froms
.
top
in
let
pre_state
=
match
!
call_froms_stack
with
...
...
@@ -168,28 +166,21 @@ let record_for_individual_froms (call_stack, value_res) =
in
if
From_parameters
.
VerifyAssigns
.
get
()
then
!
Db
.
Value
.
verify_assigns_froms
cur_kf
~
pre
:
pre_state
froms
;
(
match
value_res
with
|
Value_types
.
NormalStore
(
_
,
memexec_counter
)
->
MemExec
.
replace
memexec_counter
froms
|
_
->
()
);
MemExec
.
replace
memexec_counter
froms
;
froms
|
Value_types
.
Reuse
counter
->
|
Reuse
counter
->
MemExec
.
find
counter
in
end_record
call
_
stack
froms
end_record
callstack
froms
end
(* Register our callbacks inside the value analysis *)
let
()
=
From_parameters
.
ForceCallDeps
.
add_update_hook
(
fun
_bold
bnew
->
if
bnew
then
begin
Db
.
Value
.
Call_Type_Value_Callbacks
.
extend_once
call_for_individual_froms
;
Db
.
Value
.
Record_Value_Callbacks_New
.
extend_once
record_for_individual_froms
;
end
)
let
()
=
Eva
.
Cvalue_callbacks
.
register_call_hook
call_for_individual_froms
;
Eva
.
Cvalue_callbacks
.
register_call_results_hook
record_for_individual_froms
let
force_compute_all_calldeps
()
=
...
...
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