Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
3c11e8a7
Commit
3c11e8a7
authored
Oct 15, 2020
by
Virgile Prevosto
Browse files
[offsetmap] make fold_offset tailrec
parent
b9a92229
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/kernel_services/abstract_interp/offsetmap.ml
View file @
3c11e8a7
...
...
@@ -510,14 +510,9 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
|
Node
(
max
,
_
,
_
,
_
,
_
,
r
,
m
,
v
,
_
)
->
let
abs_max
=
max
+~
o
in
let
now
=
f
(
o
,
abs_max
)
(
v
,
m
,
r
)
pre
in
let
no
,
nt
,
nz
=
match
move_right
o
t
z
with
|
t
->
t
|
exception
End_reached
->
abs_max
,
Empty
,
z
(* End the recursion at next iteration *)
in
aux_fold
no
nt
nz
now
match
move_right
o
t
z
with
|
no
,
nt
,
nz
->
aux_fold
no
nt
nz
now
|
exception
End_reached
->
now
in
aux_fold
o
n
z
acc
;;
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment