aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/votour.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-11-22 18:31:45 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-11-22 20:08:25 +0100
commitf6f80f68c890813522fabe5787181d0eaab8695e (patch)
treea726947c7822be9f0c9343123cb1323bd697d189 /checker/votour.ml
parenteb91ccaf236bc9a60a1e216b76a0a42980c072a7 (diff)
Implement a tail-recursive traversal of the object in votour.
Diffstat (limited to 'checker/votour.ml')
-rw-r--r--checker/votour.ml21
1 files changed, 12 insertions, 9 deletions
diff --git a/checker/votour.ml b/checker/votour.ml
index 0998bb94b..7fb7aee94 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -81,22 +81,25 @@ struct
let ws = Sys.word_size / 8
- let rec init_size seen = function
- | Int _ | Atm _ | Fun _ -> 0
+ let rec init_size seen k = function
+ | Int _ | Atm _ | Fun _ -> k 0
| Ptr p ->
- if seen.(p) then 0
+ if seen.(p) then k 0
else
let () = seen.(p) <- true in
match (!memory).(p) with
| Struct (tag, os) ->
- let fold accu o = accu + 1 + init_size seen o in
- let size = Array.fold_left fold 1 os in
- let () = (!sizes).(p) <- size in
- size
+ let len = Array.length os in
+ let rec fold i accu k =
+ if i == len then k accu
+ else
+ init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i)
+ in
+ fold 0 1 (fun size -> let () = (!sizes).(p) <- size in k size)
| String s ->
let size = 2 + (String.length s / ws) in
let () = (!sizes).(p) <- size in
- size
+ k size
let size = function
| Int _ | Atm _ | Fun _ -> 0
@@ -116,7 +119,7 @@ struct
let () = memory := mem in
let () = sizes := Array.make (Array.length mem) (-1) in
let seen = Array.make (Array.length mem) false in
- let _ = init_size seen obj in
+ let () = init_size seen ignore obj in
obj
let oid = function