package linksem

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

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

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

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.

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.

OCaml

Innovation. Community. Security.