aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorMaxime Dénès2018-09-14 17:37:01 +0200
committerMaxime Dénès2018-09-17 09:33:30 +0200
commit42706b1cd101f389f3e704f859200a35316bd97e (patch)
treec3cd8dce2a510ec18367021df441b0df7e3090dc /kernel
parent7a4b3edf1a4299c7813668515ad1b8fa6cf99dd3 (diff)
Add assertion on tags in eq_structured_constants
Diffstat (limited to 'kernel')
-rw-r--r--kernel/vmvalues.ml27
1 files changed, 16 insertions, 11 deletions
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index d6970c35aa..a972803ce4 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -69,17 +69,22 @@ let rec eq_structured_values v1 v2 =
let o1 = Obj.repr v1 in
let o2 = Obj.repr v2 in
if Obj.is_int o1 && Obj.is_int o2 then o1 == o2
- else if Int.equal (Obj.tag o1) (Obj.tag o2) &&
- Int.equal (Obj.size o1) (Obj.size o2)
- then
- let i = ref 0 in
- while (!i < Obj.size o1 && eq_structured_values
- (Obj.magic (Obj.field o1 !i) : structured_values)
- (Obj.magic (Obj.field o2 !i) : structured_values)) do
- incr i
- done;
- !i >= Obj.size o1
- else false
+ else
+ let t1 = Obj.tag o1 in
+ let t2 = Obj.tag o2 in
+ if Int.equal t1 t2 &&
+ Int.equal (Obj.size o1) (Obj.size o2)
+ then begin
+ assert (t1 <= last_variant_tag && t2 <= last_variant_tag);
+ let i = ref 0 in
+ while (!i < Obj.size o1 && eq_structured_values
+ (Obj.magic (Obj.field o1 !i) : structured_values)
+ (Obj.magic (Obj.field o2 !i) : structured_values)) do
+ incr i
+ done;
+ !i >= Obj.size o1
+ end
+ else false
let hash_structured_values (v : structured_values) =
(* We may want a better hash function here *)