Skip to content

Commit

Permalink
LowParse.Low.Int32le: add assert
Browse files Browse the repository at this point in the history
Somehow fixes the build...
  • Loading branch information
mtzguido committed Dec 9, 2023
1 parent a5be4ca commit fd4da13
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/lowparse/LowParse.Low.Int32le.fst
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit fd4da13

Please sign in to comment.