From fd4da13cbc7865166b95996a0696b7cbc07a66fc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 8 Dec 2023 23:15:35 -0800 Subject: [PATCH] LowParse.Low.Int32le: add assert Somehow fixes the build... --- src/lowparse/LowParse.Low.Int32le.fst | 1 + 1 file changed, 1 insertion(+) diff --git a/src/lowparse/LowParse.Low.Int32le.fst b/src/lowparse/LowParse.Low.Int32le.fst index 98b73864e..5229850cc 100644 --- a/src/lowparse/LowParse.Low.Int32le.fst +++ b/src/lowparse/LowParse.Low.Int32le.fst @@ -15,6 +15,7 @@ inline_for_extraction let read_int32le : leaf_reader parse_int32le = make_total_constant_size_reader 4 4ul decode_int32le (decode_int32le_total_constant ()) (fun #rrel #rel b pos -> let h = HST.get () in + assert ((U32.v pos + 4) <= Seq.length (B.as_seq h b)); [@inline_let] let _ = decode_int32le_eq (Seq.slice (B.as_seq h b) (U32.v pos) (U32.v pos + 4)) in let r0 = B.index b pos in let r1 = B.index b (pos `U32.add` 1ul) in