package linksem

You can search for identifiers within the package.

in-package search v0.2.0

linksem_zarith

Legend:
Library
Module
Module type
Parameter
Class
Class type

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

val elf_dt_gnu_addrrnghi : Nat_big_num.num

val elf_dt_gnu_addrrnglo : Nat_big_num.num

val elf_dt_gnu_auxiliary : Nat_big_num.num

val elf_dt_gnu_filter : Nat_big_num.num

The following is "specified" in the LSB document but is not present in the * elf.c file so taken from elf.h from GLIBC:

val elf_dt_gnu_num : Nat_big_num.num

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

val elf_dt_gnu_posflag_1 : Nat_big_num.num

??? This should match something

val elf_dt_gnu_relcount : Nat_big_num.num

val elf_dt_gnu_relacount : Nat_big_num.num

val elf_dt_gnu_syminent : Nat_big_num.num

val elf_dt_gnu_syminfo : Nat_big_num.num

val elf_dt_gnu_syminsz : Nat_big_num.num

val elf_dt_gnu_valrnghi : Nat_big_num.num

val elf_dt_gnu_valrnglo : Nat_big_num.num

val elf_dt_gnu_verdef : Nat_big_num.num

val elf_dt_gnu_verdefnum : Nat_big_num.num

val elf_dt_gnu_verneed : Nat_big_num.num

val elf_dt_gnu_verneednum : Nat_big_num.num

val elf_dt_gnu_versym : Nat_big_num.num

Not present in the LSB but turns up in "real" ELF files...

val elf_dt_gnu_hash : Nat_big_num.num

val elf_dt_gnu_flags_1 : Nat_big_num.num

val elf_dt_gnu_checksum : Nat_big_num.num

val elf_dt_gnu_prelinked : Nat_big_num.num

Extended DT flags for FLAGS_1 dynamic section types. Taken from GLibC source * as they appear to be completely unspecified!

val gnu_df_1_now : Nat_big_num.num

val gnu_df_1_global : Nat_big_num.num

val gnu_df_1_group : Nat_big_num.num

val gnu_df_1_nodelete : Nat_big_num.num

val gnu_df_1_loadfltr : Nat_big_num.num

val gnu_df_1_initfirst : Nat_big_num.num

val gnu_df_1_noopen : Nat_big_num.num

val gnu_df_1_origin : Nat_big_num.num

val gnu_df_1_direct : Nat_big_num.num

val gnu_df_1_trans : Nat_big_num.num

val gnu_df_1_interpose : Nat_big_num.num

val gnu_df_1_nodeflib : Nat_big_num.num

val gnu_df_1_nodump : Nat_big_num.num

val gnu_df_1_confalt : Nat_big_num.num

val gnu_df_1_endfiltee : Nat_big_num.num

val gnu_df_1_dispreldne : Nat_big_num.num

val gnu_df_1_disprelpnd : Nat_big_num.num

val gnu_string_of_dt_flag_1 : Nat_big_num.num -> string

gnu_string_of_dt_flag1 m produces a string based representation of GNU * extensions flag_1 value m.

val gnu_ext_os_additional_ranges : Nat_big_num.num -> bool

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.

val string_of_gnu_ext_dynamic_tag0 : Nat_big_num.num -> string

string_of_gnu_ext_dynamic_tag0 m produces a string based representation of * GNU extensions dynamic tag value m.

val string_of_gnu_ext_dynamic_tag : Nat_big_num.num -> string

string_of_gnu_ext_dynamic_tag m produces a string based representation of * GNU extensions dynamic tag value m.