package linksem
Install
Dune Dependency
Authors
Maintainers
Sources
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/linksem_zarith/Gnu_ext_dynamic/index.html
Module Gnu_ext_dynamic
Source
gnu_ext_dynamic
contains GNU extension specific definitions related to the * .dynamic section of an ELF file.
Additional dynamic entries, see LSB section 11.3.2.2. * All values taken from elf.c from binutils and GLIBC as the LSB does not * specify them. * * 98 #define OLD_DT_LOOS 0x60000000 * 99 #define DT_LOOS 0x6000000d * 100 #define DT_HIOS 0x6ffff000 * 101 #define DT_VALRNGLO 0x6ffffd00 * 102 #define DT_VALRNGHI 0x6ffffdff * 103 #define DT_ADDRRNGLO 0x6ffffe00 * 104 #define DT_ADDRRNGHI 0x6ffffeff * 105 #define DT_VERSYM 0x6ffffff0 * 106 #define DT_RELACOUNT 0x6ffffff9 * 107 #define DT_RELCOUNT 0x6ffffffa * 108 #define DT_FLAGS_1 0x6ffffffb * 109 #define DT_VERDEF 0x6ffffffc * 110 #define DT_VERDEFNUM 0x6ffffffd * 111 #define DT_VERNEED 0x6ffffffe * 112 #define DT_VERNEEDNUM 0x6fffffff * 113 #define OLD_DT_HIOS 0x6fffffff * 114 #define DT_LOPROC 0x70000000 * 115 #define DT_HIPROC 0x7fffffff
The following is "specified" in the LSB document but is not present in the * elf.c file so taken from elf.h from GLIBC:
The following is "specified" in the LSB document but is not present in the * elf.c file so taken from elf.h from GLIBC:
??? This should match something
??? This should match something
Not present in the LSB but turns up in "real" ELF files...
Extended DT flags for FLAGS_1 dynamic section types. Taken from GLibC source * as they appear to be completely unspecified!
gnu_string_of_dt_flag1 m
produces a string based representation of GNU * extensions flag_1 value m
.
gnu_ext_os_additional_ranges m
checks whether dynamic section type m
* lies within the ranges set aside for GNU specific functionality. * NB: quite ad hoc as this is not properly specified anywhere.
val gnu_ext_tag_correspondence_of_tag0 :
Nat_big_num.num ->
Elf_dynamic.tag_correspondence Error.error
gnu_ext_tag_correspondence_of_tag0 m
produces a tag correspondence for the * extended GNU-specific dynamic section types m
. Used to provide the ABI * specific functionality expected of the corresponding function in the elf_dynamic * module.
val gnu_ext_tag_correspondence_of_tag :
Nat_big_num.num ->
Elf_dynamic.tag_correspondence Error.error
gnu_ext_tag_correspondence_of_tag m
produces a tag correspondence for the * extended GNU-specific dynamic section types m
. Used to provide the ABI * specific functionality expected of the corresponding function in the elf_dynamic * module. * TODO: examine whether this and the function above really need separating into * two functions.
val gnu_ext_elf32_value_of_elf32_dyn0 :
Elf_dynamic.elf32_dyn ->
'a ->
(Uint32_wrapper.uint32, Uint32_wrapper.uint32) Elf_dynamic.dyn_value
Error.error
gnu_ext_elf32_value_of_elf32_dyn0 dyn
extracts a dynamic value from the * dynamic section entry dyn
under the assumption that its type is a GNU * extended dynamic section type. Fails otherwise. Used to provide the * ABI-specific functionality expected of the corresponding functions in * elf_dynamic.lem.
val gnu_ext_elf64_value_of_elf64_dyn0 :
Elf_dynamic.elf64_dyn ->
'a ->
(Uint64_wrapper.uint64, Uint64_wrapper.uint64) Elf_dynamic.dyn_value
Error.error
gnu_ext_elf64_value_of_elf64_dyn0 dyn
extracts a dynamic value from the * dynamic section entry dyn
under the assumption that its type is a GNU * extended dynamic section type. Fails otherwise. Used to provide the * ABI-specific functionality expected of the corresponding functions in * elf_dynamic.lem.
val gnu_ext_elf32_value_of_elf32_dyn :
Elf_dynamic.elf32_dyn ->
'a ->
Elf_dynamic.elf32_dyn_value Error.error
gnu_ext_elf32_value_of_elf32_dyn dyn
extracts a dynamic value from the * dynamic section entry dyn
under the assumption that its type is a GNU * extended dynamic section type. Fails otherwise. Used to provide the * ABI-specific functionality expected of the corresponding functions in * elf_dynamic.lem. * TODO: some of these cases are missing as they have never come up in "real" * ELF files that have been processed as part of validation. Try and find some * files that do actually exhibit these.
val gnu_ext_elf64_value_of_elf64_dyn :
Elf_dynamic.elf64_dyn ->
'a ->
Elf_dynamic.elf64_dyn_value Error.error
gnu_ext_elf64_value_of_elf64_dyn dyn
extracts a dynamic value from the * dynamic section entry dyn
under the assumption that its type is a GNU * extended dynamic section type. Fails otherwise. Used to provide the * ABI-specific functionality expected of the corresponding functions in * elf_dynamic.lem. * TODO: some of these cases are missing as they have never come up in "real" * ELF files that have been processed as part of validation. Try and find some * files that do actually exhibit these.
string_of_gnu_ext_dynamic_tag0 m
produces a string based representation of * GNU extensions dynamic tag value m
.
string_of_gnu_ext_dynamic_tag m
produces a string based representation of * GNU extensions dynamic tag value m
.