Skip to content

Commit

Permalink
Merge pull request #119 from mtzguido/fix
Browse files Browse the repository at this point in the history
LowParse.Low.Int32le: add assert
  • Loading branch information
mtzguido authored Dec 9, 2023
2 parents a5be4ca + fd4da13 commit 4210951
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 4210951

Please sign in to comment.