From f03aaf12eb7d89fa4caa59873e114c8cd125b950 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 10 Sep 2015 11:47:21 +0200 Subject: Assertion checking that invariant enforced by 0f8d1b92 always holds. When reifying a 31-bit integer after a VM computation, we check that no bit outside the 31 LSB is set to 1. --- kernel/environ.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 109e3830c..bf12d6c6d 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -584,7 +584,10 @@ let dispatch = Array.init 31 (fun n -> mkConstruct (digit_ind, nth_digit_plus_one i (30-n))) in - mkApp(mkConstruct(ind, 1), array_of_int tag) + (* We check that no bit above 31 is set to one. This assertion used to + fail in the VM, and led to conversion tests failing at Qed. *) + assert (Int.equal (tag lsr 31) 0); + mkApp(mkConstruct(ind, 1), array_of_int tag) in (* subfunction which dispatches the compiling information of an -- cgit v1.2.3