package linksem
-
linksem_zarith
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package linksem
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
elf_relocation formalises types, functions and other definitions for working * with ELF relocation and relocation with addend entries.
ELF relocation records
type elf32_relocation = {elf32_r_offset : Uint32_wrapper.uint32;(*Address at which to relocate
*)elf32_r_info : Uint32_wrapper.uint32;(*Symbol table index/type of relocation to apply
*)
}elf32_relocation is a simple relocation record (without addend).
type elf32_relocation_a = {elf32_ra_offset : Uint32_wrapper.uint32;(*Address at which to relocate
*)elf32_ra_info : Uint32_wrapper.uint32;(*Symbol table index/type of relocation to apply
*)elf32_ra_addend : Int32.t;(*Addend used to compute value to be stored
*)
}elf32_relocation_a is a relocation record with addend.
type elf64_relocation = {elf64_r_offset : Uint64_wrapper.uint64;(*Address at which to relocate
*)elf64_r_info : Uint64_wrapper.uint64;(*Symbol table index/type of relocation to apply
*)
}elf64_relocation is a simple relocation record (without addend).
type elf64_relocation_a = {elf64_ra_offset : Uint64_wrapper.uint64;(*Address at which to relocate
*)elf64_ra_info : Uint64_wrapper.uint64;(*Symbol table index/type of relocation to apply
*)elf64_ra_addend : Int64.t;(*Addend used to compute value to be stored
*)
}elf64_relocation_a is a relocation record with addend.
val elf64_relocation_a_compare :
elf64_relocation_a ->
elf64_relocation_a ->
intelf64_relocation_a_compare r1 r2 is an ordering comparison function for * relocation with addend records suitable for constructing sets, finite map * and other ordered data structures. * NB: we exclusively use elf64_relocation_a in range tags, regardless of what * file/reloc the info came from, so only this one needs an Ord instance.
val instance_Basic_classes_Ord_Elf_relocation_elf64_relocation_a_dict :
elf64_relocation_a Lem_basic_classes.ord_classReading relocation entries
val read_elf32_relocation :
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
(elf32_relocation * Byte_sequence_wrapper.byte_sequence) Error.errorread_elf32_relocation ed bs0 parses an elf32_relocation record from * byte sequence bs0 assuming endianness ed. The suffix of bs0 remaining * after parsing is also returned. * Fails if the relocation record cannot be parsed.
val read_elf64_relocation :
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
(elf64_relocation * Byte_sequence_wrapper.byte_sequence) Error.errorread_elf64_relocation ed bs0 parses an elf64_relocation record from * byte sequence bs0 assuming endianness ed. The suffix of bs0 remaining * after parsing is also returned. * Fails if the relocation record cannot be parsed.
val read_elf32_relocation_a :
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
(elf32_relocation_a * Byte_sequence_wrapper.byte_sequence) Error.errorread_elf32_relocation_a ed bs0 parses an elf32_relocation_a record from * byte sequence bs0 assuming endianness ed. The suffix of bs0 remaining * after parsing is also returned. * Fails if the relocation record cannot be parsed.
val read_elf64_relocation_a :
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
(elf64_relocation_a * Byte_sequence_wrapper.byte_sequence) Error.errorread_elf64_relocation_a ed bs0 parses an elf64_relocation_a record from * byte sequence bs0 assuming endianness ed. The suffix of bs0 remaining * after parsing is also returned. * Fails if the relocation record cannot be parsed.
val read_elf32_relocation_section' :
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
elf32_relocation list Error.errorread_elf32_relocation_section' ed bs0 parses a list of elf32_relocation * records from byte sequence bs0, which is assumed to have the exact size * required, assuming endianness ed. * Fails if any of the records cannot be parsed.
val read_elf64_relocation_section' :
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
elf64_relocation list Error.errorread_elf64_relocation_section' ed bs0 parses a list of elf64_relocation * records from byte sequence bs0, which is assumed to have the exact size * required, assuming endianness ed. * Fails if any of the records cannot be parsed.
val read_elf32_relocation_a_section' :
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
elf32_relocation_a list Error.errorread_elf32_relocation_a_section' ed bs0 parses a list of elf32_relocation_a * records from byte sequence bs0, which is assumed to have the exact size * required, assuming endianness ed. * Fails if any of the records cannot be parsed.
val read_elf64_relocation_a_section' :
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
elf64_relocation_a list Error.errorread_elf64_relocation_a_section' ed bs0 parses a list of elf64_relocation_a * records from byte sequence bs0, which is assumed to have the exact size * required, assuming endianness ed. * Fails if any of the records cannot be parsed.
val read_elf32_relocation_section :
Nat_big_num.num ->
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
(elf32_relocation list * Byte_sequence_wrapper.byte_sequence) Error.errorread_elf32_relocation_section sz ed bs0 reads in a list of elf32_relocation * records from a prefix of bs0 of size sz assuming endianness ed. The * suffix of bs0 remaining after parsing is also returned. * Fails if any of the records cannot be parsed or if the length of bs0 is * less than sz.
val read_elf64_relocation_section :
Nat_big_num.num ->
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
(elf64_relocation list * Byte_sequence_wrapper.byte_sequence) Error.errorread_elf64_relocation_section sz ed bs0 reads in a list of elf64_relocation * records from a prefix of bs0 of size sz assuming endianness ed. The * suffix of bs0 remaining after parsing is also returned. * Fails if any of the records cannot be parsed or if the length of bs0 is * less than sz.
val read_elf32_relocation_a_section :
Nat_big_num.num ->
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
(elf32_relocation_a list * Byte_sequence_wrapper.byte_sequence) Error.errorread_elf32_relocation_a_section sz ed bs0 reads in a list of elf32_relocation_a * records from a prefix of bs0 of size sz assuming endianness ed. The * suffix of bs0 remaining after parsing is also returned. * Fails if any of the records cannot be parsed or if the length of bs0 is * less than sz.
val read_elf64_relocation_a_section :
Nat_big_num.num ->
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
(elf64_relocation_a list * Byte_sequence_wrapper.byte_sequence) Error.errorread_elf64_relocation_a_section sz ed bs0 reads in a list of elf64_relocation_a * records from a prefix of bs0 of size sz assuming endianness ed. The * suffix of bs0 remaining after parsing is also returned. * Fails if any of the records cannot be parsed or if the length of bs0 is * less than sz.