package linksem
Install
Dune Dependency
Authors
Maintainers
Sources
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/linksem_zarith/Byte_sequence/index.html
Module Byte_sequence
Source
byte_sequence.lem
, a list of bytes used for ELF I/O and other basic tasks * in the ELF model.
val read_char :
Byte_sequence_wrapper.byte_sequence ->
(char * Byte_sequence_wrapper.byte_sequence) Error.error
read_char bs0
reads a single byte from byte sequence bs0
and returns the * remainder of the byte sequence. Fails if bs0
is empty. * TODO: rename to read_byte, probably.
find_byte bs b
finds the first occurence of b in bs and gives the index. * returns Nothing
if the byte do not appear in bs
acquire fname
exhaustively reads in a byte_sequence from a file pointed to * by filename fname
. Fails if the file does not exist, or if the transcription * otherwise fails.
serialise_byte_list fname bs
writes a list of bytes, bs
, to a binary file * pointed to by filename fname
. Fails if the transcription fails. Implemented * as a primitive in OCaml.
create cnt b
creates a byte sequence of length cnt
containing only b
.
zeros cnt
creates a byte sequence of length cnt
containing only 0, the * null byte.
length bs0
returns the length of bs0
.
concat bs
concatenates a list of byte sequences, bs
, into a single byte * sequence, maintaining byte order across the sequences.
val zero_pad_to_length :
Nat_big_num.num ->
Byte_sequence_wrapper.byte_sequence ->
Byte_sequence_wrapper.byte_sequence
zero_pad_to_length len bs0
pads (on the right) consecutive zeros until the * resulting byte sequence is len
long. Returns bs0
if bs0
is already of * greater length than len
.
from_byte_lists bs
concatenates a list of bytes bs
and creates a byte * sequence from their contents. Maintains byte order in bs
.
string_of_byte_sequence bs0
converts byte sequence bs0
into a string * representation.
val equal :
Byte_sequence_wrapper.byte_sequence ->
Byte_sequence_wrapper.byte_sequence ->
bool
equal bs0 bs1
checks whether two byte sequences, bs0
and bs1
, are equal.
val dropbytes :
Nat_big_num.num ->
Byte_sequence_wrapper.byte_sequence ->
Byte_sequence_wrapper.byte_sequence Error.error
dropbytes cnt bs0
drops cnt
bytes from byte sequence bs0
. Fails if * cnt
is greater than the length of bs0
.
val takebytes :
Nat_big_num.num ->
Byte_sequence_wrapper.byte_sequence ->
Byte_sequence_wrapper.byte_sequence Error.error
takebytes cnt bs0
takes cnt
bytes from byte sequence bs0
. Fails if * cnt
is greater than the length of bs0
.
val takebytes_with_length0 :
Nat_big_num.num ->
Nat_big_num.num ->
Byte_sequence_wrapper.byte_sequence ->
Byte_sequence_wrapper.byte_sequence Error.error
val read_2_bytes_le :
Byte_sequence_wrapper.byte_sequence ->
((char * char) * Byte_sequence_wrapper.byte_sequence) Error.error
read_2_bytes_le bs0
reads two bytes from bs0
, returning them in * little-endian order, and returns the remainder of bs0
. Fails if bs0
has * length less than 2.
val read_2_bytes_be :
Byte_sequence_wrapper.byte_sequence ->
((char * char) * Byte_sequence_wrapper.byte_sequence) Error.error
read_2_bytes_be bs0
reads two bytes from bs0
, returning them in * big-endian order, and returns the remainder of bs0
. Fails if bs0
has * length less than 2.
val read_4_bytes_le :
Byte_sequence_wrapper.byte_sequence ->
((char * char * char * char) * Byte_sequence_wrapper.byte_sequence)
Error.error
read_4_bytes_le bs0
reads four bytes from bs0
, returning them in * little-endian order, and returns the remainder of bs0
. Fails if bs0
has * length less than 4.
val read_4_bytes_be :
Byte_sequence_wrapper.byte_sequence ->
((char * char * char * char) * Byte_sequence_wrapper.byte_sequence)
Error.error
read_4_bytes_be bs0
reads four bytes from bs0
, returning them in * big-endian order, and returns the remainder of bs0
. Fails if bs0
has * length less than 4.
val read_8_bytes_le :
Byte_sequence_wrapper.byte_sequence ->
((char * char * char * char * char * char * char * char)
* Byte_sequence_wrapper.byte_sequence)
Error.error
read_8_bytes_le bs0
reads eight bytes from bs0
, returning them in * little-endian order, and returns the remainder of bs0
. Fails if bs0
has * length less than 8.
val read_8_bytes_be :
Byte_sequence_wrapper.byte_sequence ->
((char * char * char * char * char * char * char * char)
* Byte_sequence_wrapper.byte_sequence)
Error.error
read_8_bytes_be bs0
reads eight bytes from bs0
, returning them in * big-endian order, and returns the remainder of bs0
. Fails if bs0
has * length less than 8.
val partition0 :
Nat_big_num.num ->
Byte_sequence_wrapper.byte_sequence ->
(Byte_sequence_wrapper.byte_sequence * Byte_sequence_wrapper.byte_sequence)
Error.error
partition pnt bs0
splits bs0
into two parts at index pnt
. Fails if * pnt
is greater than the length of bs0
.
val partition_with_length :
Nat_big_num.num ->
Nat_big_num.num ->
Byte_sequence_wrapper.byte_sequence ->
(Byte_sequence_wrapper.byte_sequence * Byte_sequence_wrapper.byte_sequence)
Error.error
val offset_and_cut :
Nat_big_num.num ->
Nat_big_num.num ->
Byte_sequence_wrapper.byte_sequence ->
Byte_sequence_wrapper.byte_sequence Error.error
offset_and_cut off cut bs0
first cuts off
bytes off bs0
, then cuts * the resulting byte sequence to length cut
. Fails if off
is greater than * the length of bs0
and if cut
is greater than the length of the intermediate * byte sequence.