package linksem

byte_sequence.lem, a list of bytes used for ELF I/O and other basic tasks * in the ELF model.

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.

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.

equal bs0 bs1 checks whether two byte sequences, bs0 and bs1, are equal.

dropbytes cnt bs0 drops cnt bytes from byte sequence bs0. Fails if * cnt is greater than the length of bs0.

takebytes cnt bs0 takes cnt bytes from byte sequence bs0. Fails if * cnt is greater than the length of bs0.

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.

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.

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.

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.

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.

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.

partition pnt bs0 splits bs0 into two parts at index pnt. Fails if * pnt is greater than the length of bs0.

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.