package linksem
Install
Dune Dependency
Authors
Maintainers
Sources
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/linksem_zarith/Gnu_ext_note/index.html
Module Gnu_ext_noteSource
gnu_ext_note contains GNU extension specific definitions relating to the * .note section/segment of an ELF file.
The following two functions are utility functions to convert a list of bytes * into words, ready for further processing into strings.
val group_elf32_words :
Endianness.endianness ->
char list ->
Uint32_wrapper.uint32 list Error.errorval group_elf64_words :
Endianness.endianness ->
char list ->
Uint32_wrapper.uint32 list Error.errorval gnu_ext_check_elf32_abi_note_tag_section :
Endianness.endianness ->
Elf_section_header_table.elf32_section_header_table_entry list ->
String_table.string_table ->
Byte_sequence_wrapper.byte_sequence ->
boolgnu_ext_check_elf32_abi_note_tag_section endain sht stbl bs0 checks the * .note.ABI-tag section of an ELF file to ensure conformance with the GNU * extensions. The string in this note should contain the string "GNU".
val gnu_ext_check_elf64_abi_note_tag_section :
Endianness.endianness ->
Elf_section_header_table.elf64_section_header_table_entry list ->
String_table.string_table ->
Byte_sequence_wrapper.byte_sequence ->
boolgnu_ext_check_elf64_abi_note_tag_section endain sht stbl bs0 checks the * .note.ABI-tag section of an ELF file to ensure conformance with the GNU * extensions. The string in this note should contain the string "GNU".
val gnu_ext_extract_elf32_earliest_compatible_kernel :
Endianness.endianness ->
Elf_section_header_table.elf32_section_header_table_entry list ->
String_table.string_table ->
Byte_sequence_wrapper.byte_sequence ->
string Error.errorgnu_ext_extract_elf32_earliest_compatible_kernel end sht stab bs0 extracts * the earliest compatible Linux kernel with the given ELF file from its section * header table sht, and string table stbl, assuming endianness endian. * NB: marked as OCaml only as need to extract a string from integers. * TODO: implement some string parsing functions in Isabelle/HOL so things like * this can be extracted.
val gnu_ext_extract_elf64_earliest_compatible_kernel :
Endianness.endianness ->
Elf_section_header_table.elf64_section_header_table_entry list ->
String_table.string_table ->
Byte_sequence_wrapper.byte_sequence ->
string Error.errorgnu_ext_extract_elf64_earliest_compatible_kernel end sht stab bs0 extracts * the earliest compatible Linux kernel with the given ELF file from its section * header table sht, and string table stbl, assuming endianness endian. * NB: marked as OCaml only as need to extract a string from integers. * TODO: implement some string parsing functions in Isabelle/HOL so things like * this can be extracted.