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
2c0c547f
Commit
2c0c547f
authored
3 years ago
by
Basile Desloges
Browse files
Options
Downloads
Patches
Plain Diff
[eacsl] Remove unused env parameter from inject_in_global
parent
33956f4f
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/e-acsl/src/code_generator/injector.ml
+9
-9
9 additions, 9 deletions
src/plugins/e-acsl/src/code_generator/injector.ml
with
9 additions
and
9 deletions
src/plugins/e-acsl/src/code_generator/injector.ml
+
9
−
9
View file @
2c0c547f
...
...
@@ -602,7 +602,7 @@ let inject_in_fundec main fundec =
let
main
=
if
Kernel_function
.
is_main
kf
then
Some
kf
else
main
in
Options
.
feedback
~
dkey
~
level
:
2
"function %a done."
Kernel_function
.
pretty
kf
;
env
,
main
main
(* ************************************************************************** *)
(* The whole AST *)
...
...
@@ -621,26 +621,26 @@ let unghost_vi vi =
|
_
->
()
let
inject_in_global
(
env
,
main
)
global
=
let
update_builtin
vi
=
Builtins
.
update
vi
.
vname
vi
;
env
,
main
in
let
inject_in_global
main
global
=
let
update_builtin
vi
=
Builtins
.
update
vi
.
vname
vi
;
main
in
let
observe_and_unghost
vi
=
unghost_vi
vi
;
Global_observer
.
add
vi
;
env
,
main
unghost_vi
vi
;
Global_observer
.
add
vi
;
main
in
let
var_def
vi
init
=
Global_observer
.
add
vi
;
unghost_vi
vi
;
let
_init
,
env
=
inject_in_init
e
nv
None
vi
NoOffset
init
in
let
_init
,
_
env
=
inject_in_init
E
nv
.
empty
None
vi
NoOffset
init
in
(* ignore the new initializer that handles literal strings
since they are not substituted in global initializers
(see [replace_literal_string_in_exp]) *)
env
,
main
main
in
let
fun_def
({
svar
=
vi
}
as
fundec
)
=
unghost_vi
vi
;
inject_in_fundec
main
fundec
in
E_acsl_visitor
.
case_globals
~
default
:
(
fun
()
->
env
,
main
)
~
default
:
(
fun
()
->
main
)
~
builtin
:
update_builtin
~
var_fun_decl
:
observe_and_unghost
~
var_init
:
observe_and_unghost
...
...
@@ -804,8 +804,8 @@ let inject_mtracking_handler main =
end
let
inject_in_file
file
=
let
_env
,
main
=
List
.
fold_left
inject_in_global
(
Env
.
empty
,
None
)
file
.
globals
let
main
=
List
.
fold_left
inject_in_global
None
file
.
globals
in
(* post-treatment *)
(* extend [main] with forward initialization and put it at end *)
...
...
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