package linksem

You can search for identifiers within the package.

in-package search v0.2.0

package linksem

linksem_zarith

Legend:
Library
Module
Module type
Parameter
Class
Class type

val shn_undef : Nat_big_num.num

val shn_xindex : Nat_big_num.num

val elf_ft_none : Nat_big_num.num

val elf_ft_rel : Nat_big_num.num

val elf_ft_exec : Nat_big_num.num

val elf_ft_dyn : Nat_big_num.num

val elf_ft_core : Nat_big_num.num

val elf_ft_lo_os : Nat_big_num.num

val elf_ft_hi_os : Nat_big_num.num

val elf_ft_lo_proc : Nat_big_num.num

val elf_ft_hi_proc : Nat_big_num.num

val string_of_elf_file_type : 
  (Nat_big_num.num -> string) ->
  (Nat_big_num.num -> string) ->
  Nat_big_num.num ->
  string

val is_operating_system_specific_object_file_type_value : 
  Nat_big_num.num ->
  bool

val is_processor_specific_object_file_type_value : Nat_big_num.num -> bool

val elf_ma_riscv : Nat_big_num.num

val elf_ma_amdgpu : Nat_big_num.num

val elf_ma_moxie : Nat_big_num.num

val elf_ma_ft32 : Nat_big_num.num

val elf_ma_visium : Nat_big_num.num

val elf_ma_z80 : Nat_big_num.num

val elf_ma_kalimba : Nat_big_num.num

val elf_ma_norc : Nat_big_num.num

val elf_ma_cool : Nat_big_num.num

val elf_ma_coge : Nat_big_num.num

val elf_ma_cdp : Nat_big_num.num

val elf_ma_kvarc : Nat_big_num.num

val elf_ma_kmx8 : Nat_big_num.num

val elf_ma_kmx16 : Nat_big_num.num

val elf_ma_kmx32 : Nat_big_num.num

val elf_ma_km32 : Nat_big_num.num

val elf_ma_mchp_pic : Nat_big_num.num

val elf_ma_xcore : Nat_big_num.num

val elf_ma_ba2 : Nat_big_num.num

val elf_ma_ba1 : Nat_big_num.num

val elf_ma_5600ex : Nat_big_num.num

val elf_ma_78kor : Nat_big_num.num

val elf_ma_videocore5 : Nat_big_num.num

val elf_ma_rl78 : Nat_big_num.num

val elf_ma_open8 : Nat_big_num.num

val elf_ma_arc_compact2 : Nat_big_num.num

val elf_ma_corea_2nd : Nat_big_num.num

val elf_ma_corea_1st : Nat_big_num.num

val elf_ma_cloudshield : Nat_big_num.num

val elf_ma_sle9x : Nat_big_num.num

val elf_ma_l10m : Nat_big_num.num

val elf_ma_k10m : Nat_big_num.num

val elf_ma_aarch64 : Nat_big_num.num

val elf_ma_avr32 : Nat_big_num.num

val elf_ma_stm8 : Nat_big_num.num

val elf_ma_tile64 : Nat_big_num.num

val elf_ma_tilepro : Nat_big_num.num

val elf_ma_microblaze : Nat_big_num.num

val elf_ma_cuda : Nat_big_num.num

val elf_ma_tilegx : Nat_big_num.num

val elf_ma_cypress : Nat_big_num.num

val elf_ma_r32c : Nat_big_num.num

val elf_ma_trimedia : Nat_big_num.num

val elf_ma_qdsp6 : Nat_big_num.num

val elf_ma_8051 : Nat_big_num.num

val elf_ma_stxp7x : Nat_big_num.num

val elf_ma_nds32 : Nat_big_num.num

val elf_ma_ecog1x : Nat_big_num.num

val elf_ma_maxq30 : Nat_big_num.num

val elf_ma_ximo16 : Nat_big_num.num

val elf_ma_manik : Nat_big_num.num

val elf_ma_craynv2 : Nat_big_num.num

val elf_ma_rx : Nat_big_num.num

val elf_ma_metag : Nat_big_num.num

val elf_ma_mcst_elbrus : Nat_big_num.num

val elf_ma_ecog16 : Nat_big_num.num

val elf_ma_cr16 : Nat_big_num.num

val elf_ma_etpu : Nat_big_num.num

val elf_ma_tsk3000 : Nat_big_num.num

val elf_ma_rs08 : Nat_big_num.num

val elf_ma_sharc : Nat_big_num.num

val elf_ma_ecog2 : Nat_big_num.num

val elf_ma_ccore7 : Nat_big_num.num

val elf_ma_dsp24 : Nat_big_num.num

val elf_ma_videocore3 : Nat_big_num.num

val elf_ma_latticemico32 : Nat_big_num.num

val elf_ma_c17 : Nat_big_num.num

val elf_ma_c6000 : Nat_big_num.num

val elf_ma_c2000 : Nat_big_num.num

val elf_ma_c5500 : Nat_big_num.num

val elf_ma_mmdsp_plus : Nat_big_num.num

val elf_ma_zsp : Nat_big_num.num

val elf_ma_mmix : Nat_big_num.num

val elf_ma_huany : Nat_big_num.num

val elf_ma_prism : Nat_big_num.num

val elf_ma_avr : Nat_big_num.num

val elf_ma_fr30 : Nat_big_num.num

val elf_ma_d10v : Nat_big_num.num

val elf_ma_d30v : Nat_big_num.num

val elf_ma_v850 : Nat_big_num.num

val elf_ma_m32r : Nat_big_num.num

val elf_ma_mn10300 : Nat_big_num.num

val elf_ma_mn10200 : Nat_big_num.num

val elf_ma_pj : Nat_big_num.num

val elf_ma_openrisc : Nat_big_num.num

val elf_ma_arc_compact : Nat_big_num.num

val elf_ma_xtensa : Nat_big_num.num

val elf_ma_videocore : Nat_big_num.num

val elf_ma_tmm_gpp : Nat_big_num.num

val elf_ma_ns32k : Nat_big_num.num

val elf_ma_tpc : Nat_big_num.num

val elf_ma_snp1k : Nat_big_num.num

val elf_ma_st200 : Nat_big_num.num

val elf_ma_ip2k : Nat_big_num.num

val elf_ma_max : Nat_big_num.num

val elf_ma_cr : Nat_big_num.num

val elf_ma_f2mc16 : Nat_big_num.num

val elf_ma_msp430 : Nat_big_num.num

val elf_ma_blackfin : Nat_big_num.num

val elf_ma_se_c33 : Nat_big_num.num

val elf_ma_sep : Nat_big_num.num

val elf_ma_arca : Nat_big_num.num

val elf_ma_unicore : Nat_big_num.num

val elf_ma_excess : Nat_big_num.num

val elf_ma_dxp : Nat_big_num.num

val elf_ma_altera_nios2 : Nat_big_num.num

val elf_ma_crx : Nat_big_num.num

val elf_ma_xgate : Nat_big_num.num

val elf_ma_c166 : Nat_big_num.num

val elf_ma_m16c : Nat_big_num.num

val elf_ma_dspic30f : Nat_big_num.num

val elf_ma_ce : Nat_big_num.num

val elf_ma_m32c : Nat_big_num.num

val elf_ma_none : Nat_big_num.num

val elf_ma_m32 : Nat_big_num.num

val elf_ma_sparc : Nat_big_num.num

val elf_ma_386 : Nat_big_num.num

val elf_ma_68k : Nat_big_num.num

val elf_ma_88k : Nat_big_num.num

val elf_ma_860 : Nat_big_num.num

val elf_ma_mips : Nat_big_num.num

val elf_ma_s370 : Nat_big_num.num

val elf_ma_mips_rs3_le : Nat_big_num.num

val elf_ma_parisc : Nat_big_num.num

val elf_ma_vpp500 : Nat_big_num.num

val elf_ma_sparc32plus : Nat_big_num.num

val elf_ma_960 : Nat_big_num.num

val elf_ma_ppc : Nat_big_num.num

val elf_ma_ppc64 : Nat_big_num.num

val elf_ma_s390 : Nat_big_num.num

val elf_ma_spu : Nat_big_num.num

val elf_ma_v800 : Nat_big_num.num

val elf_ma_fr20 : Nat_big_num.num

val elf_ma_rh32 : Nat_big_num.num

val elf_ma_rce : Nat_big_num.num

val elf_ma_arm : Nat_big_num.num

val elf_ma_alpha : Nat_big_num.num

val elf_ma_sh : Nat_big_num.num

val elf_ma_sparcv9 : Nat_big_num.num

val elf_ma_tricore : Nat_big_num.num

val elf_ma_arc : Nat_big_num.num

val elf_ma_h8_300 : Nat_big_num.num

val elf_ma_h8_300h : Nat_big_num.num

val elf_ma_h8s : Nat_big_num.num

val elf_ma_h8_500 : Nat_big_num.num

val elf_ma_ia_64 : Nat_big_num.num

val elf_ma_mips_x : Nat_big_num.num

val elf_ma_coldfire : Nat_big_num.num

val elf_ma_68hc12 : Nat_big_num.num

val elf_ma_mma : Nat_big_num.num

val elf_ma_pcp : Nat_big_num.num

val elf_ma_ncpu : Nat_big_num.num

val elf_ma_ndr1 : Nat_big_num.num

val elf_ma_starcore : Nat_big_num.num

val elf_ma_me16 : Nat_big_num.num

val elf_ma_st100 : Nat_big_num.num

val elf_ma_tinyj : Nat_big_num.num

val elf_ma_x86_64 : Nat_big_num.num

val elf_ma_pdsp : Nat_big_num.num

val elf_ma_pdp10 : Nat_big_num.num

val elf_ma_pdp11 : Nat_big_num.num

val elf_ma_fx66 : Nat_big_num.num

val elf_ma_st9plus : Nat_big_num.num

val elf_ma_st7 : Nat_big_num.num

val elf_ma_68hc16 : Nat_big_num.num

val elf_ma_68hc11 : Nat_big_num.num

val elf_ma_68hc08 : Nat_big_num.num

val elf_ma_68hc05 : Nat_big_num.num

val elf_ma_svx : Nat_big_num.num

val elf_ma_st19 : Nat_big_num.num

val elf_ma_vax : Nat_big_num.num

val elf_ma_cris : Nat_big_num.num

val elf_ma_javelin : Nat_big_num.num

val elf_ma_firepath : Nat_big_num.num

val elf_ma_intel209 : Nat_big_num.num

val elf_ma_intel208 : Nat_big_num.num

val elf_ma_intel207 : Nat_big_num.num

val elf_ma_intel206 : Nat_big_num.num

val elf_ma_intel205 : Nat_big_num.num

val elf_ma_intel182 : Nat_big_num.num

val elf_ma_arm184 : Nat_big_num.num

val elf_ma_reserved6 : Nat_big_num.num

val elf_ma_reserved11 : Nat_big_num.num

val elf_ma_reserved12 : Nat_big_num.num

val elf_ma_reserved13 : Nat_big_num.num

val elf_ma_reserved14 : Nat_big_num.num

val elf_ma_reserved16 : Nat_big_num.num

val elf_ma_reserved24 : Nat_big_num.num

val elf_ma_reserved25 : Nat_big_num.num

val elf_ma_reserved26 : Nat_big_num.num

val elf_ma_reserved27 : Nat_big_num.num

val elf_ma_reserved28 : Nat_big_num.num

val elf_ma_reserved29 : Nat_big_num.num

val elf_ma_reserved30 : Nat_big_num.num

val elf_ma_reserved31 : Nat_big_num.num

val elf_ma_reserved32 : Nat_big_num.num

val elf_ma_reserved33 : Nat_big_num.num

val elf_ma_reserved34 : Nat_big_num.num

val elf_ma_reserved35 : Nat_big_num.num

val elf_ma_reserved121 : Nat_big_num.num

val elf_ma_reserved122 : Nat_big_num.num

val elf_ma_reserved123 : Nat_big_num.num

val elf_ma_reserved124 : Nat_big_num.num

val elf_ma_reserved125 : Nat_big_num.num

val elf_ma_reserved126 : Nat_big_num.num

val elf_ma_reserved127 : Nat_big_num.num

val elf_ma_reserved128 : Nat_big_num.num

val elf_ma_reserved129 : Nat_big_num.num

val elf_ma_reserved130 : Nat_big_num.num

val elf_ma_reserved143 : Nat_big_num.num

val elf_ma_reserved144 : Nat_big_num.num

val elf_ma_reserved145 : Nat_big_num.num

val elf_ma_reserved146 : Nat_big_num.num

val elf_ma_reserved147 : Nat_big_num.num

val elf_ma_reserved148 : Nat_big_num.num

val elf_ma_reserved149 : Nat_big_num.num

val elf_ma_reserved150 : Nat_big_num.num

val elf_ma_reserved151 : Nat_big_num.num

val elf_ma_reserved152 : Nat_big_num.num

val elf_ma_reserved153 : Nat_big_num.num

val elf_ma_reserved154 : Nat_big_num.num

val elf_ma_reserved155 : Nat_big_num.num

val elf_ma_reserved156 : Nat_big_num.num

val elf_ma_reserved157 : Nat_big_num.num

val elf_ma_reserved158 : Nat_big_num.num

val elf_ma_reserved159 : Nat_big_num.num

val string_of_elf_machine_architecture : Nat_big_num.num -> string

val elf_ev_none : Nat_big_num.num

val elf_ev_current : Nat_big_num.num

val string_of_elf_version_number : Nat_big_num.num -> string

val is_valid_extended_version_number : Nat_big_num.num -> bool

val elf_ii_mag0 : Nat_big_num.num

val elf_ii_mag1 : Nat_big_num.num

val elf_ii_mag2 : Nat_big_num.num

val elf_ii_mag3 : Nat_big_num.num

val elf_ii_class : Nat_big_num.num

val elf_ii_data : Nat_big_num.num

val elf_ii_version : Nat_big_num.num

val elf_ii_osabi : Nat_big_num.num

val elf_ii_abiversion : Nat_big_num.num

val elf_ii_pad : Nat_big_num.num

val elf_ii_nident : Nat_big_num.num

val elf_mn_mag0 : Uint32_wrapper.uint32

val elf_mn_mag1 : Uint32_wrapper.uint32

val elf_mn_mag2 : Uint32_wrapper.uint32

val elf_mn_mag3 : Uint32_wrapper.uint32

val elf_class_none : Nat_big_num.num

val elf_class_32 : Nat_big_num.num

val elf_class_64 : Nat_big_num.num

val string_of_elf_file_class : Nat_big_num.num -> string

val elf_data_none : Nat_big_num.num

val elf_data_2lsb : Nat_big_num.num

val elf_data_2msb : Nat_big_num.num

val string_of_elf_data_encoding : Nat_big_num.num -> string

val elf_osabi_none : Nat_big_num.num

val elf_osabi_hpux : Nat_big_num.num

val elf_osabi_netbsd : Nat_big_num.num

val elf_osabi_gnu : Nat_big_num.num

val elf_osabi_linux : Nat_big_num.num

val elf_osabi_solaris : Nat_big_num.num

val elf_osabi_aix : Nat_big_num.num

val elf_osabi_irix : Nat_big_num.num

val elf_osabi_freebsd : Nat_big_num.num

val elf_osabi_tru64 : Nat_big_num.num

val elf_osabi_modesto : Nat_big_num.num

val elf_osabi_openbsd : Nat_big_num.num

val elf_osabi_openvms : Nat_big_num.num

val elf_osabi_nsk : Nat_big_num.num

val elf_osabi_aros : Nat_big_num.num

val elf_osabi_fenixos : Nat_big_num.num

val elf_osabi_cloudabi : Nat_big_num.num

val elf_osabi_openvos : Nat_big_num.num

val is_valid_architecture_defined_osabi_version : Nat_big_num.num -> bool

val string_of_elf_osabi_version : 
  (Nat_big_num.num -> string) ->
  Nat_big_num.num ->
  string

val ei_nident : Nat_big_num.num

type elf32_header = {

elf32_ident : Uint32_wrapper.uint32 list;
elf32_type : Uint32_wrapper.uint32;
elf32_machine : Uint32_wrapper.uint32;
elf32_version : Uint32_wrapper.uint32;
elf32_entry : Uint32_wrapper.uint32;
elf32_phoff : Uint32_wrapper.uint32;
elf32_shoff : Uint32_wrapper.uint32;
elf32_flags : Uint32_wrapper.uint32;
elf32_ehsize : Uint32_wrapper.uint32;
elf32_phentsize : Uint32_wrapper.uint32;
elf32_phnum : Uint32_wrapper.uint32;
elf32_shentsize : Uint32_wrapper.uint32;
elf32_shnum : Uint32_wrapper.uint32;
elf32_shstrndx : Uint32_wrapper.uint32;

}

type elf64_header = {

elf64_ident : Uint32_wrapper.uint32 list;
elf64_type : Uint32_wrapper.uint32;
elf64_machine : Uint32_wrapper.uint32;
elf64_version : Uint32_wrapper.uint32;
elf64_entry : Uint64_wrapper.uint64;
elf64_phoff : Uint64_wrapper.uint64;
elf64_shoff : Uint64_wrapper.uint64;
elf64_flags : Uint32_wrapper.uint32;
elf64_ehsize : Uint32_wrapper.uint32;
elf64_phentsize : Uint32_wrapper.uint32;
elf64_phnum : Uint32_wrapper.uint32;
elf64_shentsize : Uint32_wrapper.uint32;
elf64_shnum : Uint32_wrapper.uint32;
elf64_shstrndx : Uint32_wrapper.uint32;

}

val is_valid_elf32_header : elf32_header -> bool

val is_valid_elf64_header : elf64_header -> bool

val elf32_header_compare : elf32_header -> elf32_header -> int

val instance_Basic_classes_Ord_Elf_header_elf32_header_dict : 
  elf32_header Lem_basic_classes.ord_class

val elf64_header_compare : elf64_header -> elf64_header -> int

val instance_Basic_classes_Ord_Elf_header_elf64_header_dict : 
  elf64_header Lem_basic_classes.ord_class

val is_elf32_executable_file : elf32_header -> bool

val is_elf64_executable_file : 'a -> bool

val is_elf32_shared_object_file : elf32_header -> bool

val is_elf64_shared_object_file : elf64_header -> bool

val is_elf32_relocatable_file : elf32_header -> bool

val is_elf64_relocatable_file : elf64_header -> bool

val is_elf32_linkable_file : elf32_header -> bool

val is_elf64_linkable_file : elf64_header -> bool

val get_elf32_machine_architecture : elf32_header -> Nat_big_num.num

val get_elf64_machine_architecture : elf64_header -> Nat_big_num.num

val get_elf32_osabi : elf32_header -> Nat_big_num.num

val get_elf64_osabi : elf64_header -> Nat_big_num.num

val get_elf32_data_encoding : elf32_header -> Nat_big_num.num

val get_elf64_data_encoding : elf64_header -> Nat_big_num.num

val get_elf32_file_class : elf32_header -> Nat_big_num.num

val get_elf64_file_class : elf64_header -> Nat_big_num.num

val get_elf32_version_number : elf32_header -> Nat_big_num.num

val get_elf64_version_number : elf64_header -> Nat_big_num.num

val is_valid_elf32_version_numer : elf32_header -> bool

val is_valid_elf64_version_numer : elf64_header -> bool

val get_elf32_abi_version : elf32_header -> Nat_big_num.num

val get_elf64_abi_version : elf64_header -> Nat_big_num.num

val deduce_endianness : Uint32_wrapper.uint32 list -> Endianness.endianness

val get_elf32_header_endianness : elf32_header -> Endianness.endianness

val get_elf64_header_endianness : elf64_header -> Endianness.endianness

val has_elf32_header_associated_entry_point : elf32_header -> bool

val has_elf64_header_associated_entry_point : elf64_header -> bool

val has_elf32_header_string_table : elf32_header -> bool

val has_elf64_header_string_table : elf64_header -> bool

val is_elf32_header_section_size_in_section_header_table : elf32_header -> bool

val is_elf64_header_section_size_in_section_header_table : elf64_header -> bool

val is_elf32_header_string_table_index_in_link : elf32_header -> bool

val is_elf64_header_string_table_index_in_link : elf64_header -> bool

type hdr_print_bundle =
  (Nat_big_num.num -> string) * (Nat_big_num.num -> string)

val string_of_elf32_header : 
  ((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) ->
  elf32_header ->
  string

val string_of_elf64_header : 
  ((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) ->
  elf64_header ->
  string

val string_of_elf32_header_default : elf32_header -> string

val string_of_elf64_header_default : elf64_header -> string

val instance_Show_Show_Elf_header_elf32_header_dict : 
  elf32_header Show.show_class

val instance_Show_Show_Elf_header_elf64_header_dict : 
  elf64_header Show.show_class

val read_elf_ident : 
  Byte_sequence_wrapper.byte_sequence ->
  (Uint32_wrapper.uint32 list * Byte_sequence_wrapper.byte_sequence)
    Error.error

val bytes_of_elf32_header : elf32_header -> Byte_sequence_wrapper.byte_sequence

val bytes_of_elf64_header : elf64_header -> Byte_sequence_wrapper.byte_sequence

val is_elf32_header_padding_correct : elf32_header -> bool

val is_magic_number_correct : Uint32_wrapper.uint32 list -> bool

val read_elf32_header : 
  Byte_sequence_wrapper.byte_sequence ->
  (elf32_header * Byte_sequence_wrapper.byte_sequence) Error.error

val read_elf64_header : 
  Byte_sequence_wrapper.byte_sequence ->
  (elf64_header * Byte_sequence_wrapper.byte_sequence) Error.error

val is_elf32_header_class_correct : elf32_header -> bool

val is_elf64_header_class_correct : elf64_header -> bool

val is_elf32_header_version_correct : elf32_header -> bool

val is_elf64_header_version_correct : elf64_header -> bool

val is_elf32_header_valid : elf32_header -> bool

val get_elf32_header_program_table_size : elf32_header -> Nat_big_num.num

val get_elf64_header_program_table_size : elf64_header -> Nat_big_num.num

val is_elf32_header_section_table_present : elf32_header -> bool

val is_elf64_header_section_table_present : elf64_header -> bool

val get_elf32_header_section_table_size : elf32_header -> Nat_big_num.num

val get_elf64_header_section_table_size : elf64_header -> Nat_big_num.num