linksem 0.8 · OCaml Package

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.error

val group_elf64_words : 
  Endianness.endianness ->
  char list ->
  Uint32_wrapper.uint32 list Error.error

val 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 ->
  bool

gnu_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 ->
  bool

gnu_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.error

gnu_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.error

gnu_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.

package linksem