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
c4a577f0
Commit
c4a577f0
authored
4 years ago
by
David Bühler
Browse files
Options
Downloads
Patches
Plain Diff
[Eva] In recursion.ml, uses Cil.copyVarinfo instead of makeVarinfo.
parent
5c40a23c
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/recursion.ml
+4
-13
4 additions, 13 deletions
src/plugins/value/engine/recursion.ml
with
4 additions
and
13 deletions
src/plugins/value/engine/recursion.ml
+
4
−
13
View file @
c4a577f0
...
@@ -126,18 +126,9 @@ module VarStack =
...
@@ -126,18 +126,9 @@ module VarStack =
let
size
=
9
let
size
=
9
end
)
end
)
let
copy_variable
depth
varinfo
=
let
copy_variable
fundec
depth
varinfo
=
let
name
=
Format
.
asprintf
"
\\
copy<%s>[%i]"
varinfo
.
vname
depth
let
name
=
Format
.
asprintf
"
\\
copy<%s>[%i]"
varinfo
.
vname
depth
in
and
typ
=
varinfo
.
vtype
let
v
=
Cil
.
copyVarinfo
varinfo
name
in
and
source
=
true
and
temp
=
varinfo
.
vtemp
and
referenced
=
varinfo
.
vreferenced
and
ghost
=
varinfo
.
vghost
and
loc
=
varinfo
.
vdecl
in
Cil
.
makeVarinfo
~
source
~
temp
~
referenced
~
ghost
~
loc
false
false
name
typ
let
copy_fresh_variable
fundec
depth
varinfo
=
let
v
=
copy_variable
depth
varinfo
in
Cil
.
refresh_local_name
fundec
v
;
Cil
.
refresh_local_name
fundec
v
;
v
v
...
@@ -147,7 +138,7 @@ let make_stack (kf, depth) =
...
@@ -147,7 +138,7 @@ let make_stack (kf, depth) =
with
Kernel_function
.
No_Definition
->
assert
false
with
Kernel_function
.
No_Definition
->
assert
false
in
in
let
vars
=
Kernel_function
.(
get_formals
kf
@
get_locals
kf
)
in
let
vars
=
Kernel_function
.(
get_formals
kf
@
get_locals
kf
)
in
let
copy
v
=
v
,
copy_
fresh_
variable
fundec
depth
v
in
let
copy
v
=
v
,
copy_variable
fundec
depth
v
in
List
.
map
copy
vars
List
.
map
copy
vars
let
get_stack
kf
depth
=
VarStack
.
memo
make_stack
(
kf
,
depth
)
let
get_stack
kf
depth
=
VarStack
.
memo
make_stack
(
kf
,
depth
)
...
...
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