package linksem
A formalisation of the core ELF and DWARF file formats written in Lem
Install
Dune Dependency
Authors
Maintainers
Sources
0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/src/linksem_zarith/abi_cheri_mips64_elf_header.ml.html
Source file abi_cheri_mips64_elf_header.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58(*Generated by Lem from abis/cheri_mips64/abi_cheri_mips64_elf_header.lem.*) open Lem_basic_classes open Lem_bool open Lem_list open Lem_num open Lem_maybe open Missing_pervasives open Elf_header open Elf_types_native_uint open Endianness (*val abi_cheri_mips64_data_encoding : natural*) let abi_cheri_mips64_data_encoding:Nat_big_num.num= elf_data_2msb (*val abi_cheri_mips64_endianness : endianness*) let abi_cheri_mips64_endianness:endianness= Big (* Must match above *) (*val abi_cheri_mips64_file_class : natural*) let abi_cheri_mips64_file_class:Nat_big_num.num= elf_class_64 (*val abi_cheri_mips64_file_version : natural*) let abi_cheri_mips64_file_version:Nat_big_num.num= elf_ev_current (*val abi_cheri_mips64_page_size_min : natural*) let abi_cheri_mips64_page_size_min:Nat_big_num.num= ( (Nat_big_num.of_int 4096)) (*val abi_cheri_mips64_page_size_max : natural*) let abi_cheri_mips64_page_size_max:Nat_big_num.num= ( (Nat_big_num.of_int 65536)) let ef_mips_abi_cheriabi : Nat_big_num.num= (natural_of_hex "0x0000C000") let ef_mips_mach_cheri128 : Nat_big_num.num= (natural_of_hex "0x00C10000") let ef_mips_mach_cheri256 : Nat_big_num.num= (natural_of_hex "0x00C20000") (*val is_valid_abi_cheri_mips64_machine_architecture : natural -> bool*) let is_valid_abi_cheri_mips64_machine_architecture m:bool= (Nat_big_num.equal m elf_ma_mips) (*val is_valid_abi_cheri_mips64_magic_number : list unsigned_char -> bool*) let is_valid_abi_cheri_mips64_magic_number magic:bool= ((match Lem_list.list_index magic (Nat_big_num.to_int elf_ii_class) with | None -> false | Some cls -> (match Lem_list.list_index magic (Nat_big_num.to_int elf_ii_data) with | None -> false | Some data -> ( Nat_big_num.equal(Uint32_wrapper.to_bigint cls) abi_cheri_mips64_file_class) && ( Nat_big_num.equal(Uint32_wrapper.to_bigint data) abi_cheri_mips64_data_encoding) ) )) (*val is_pure_abi_cheri_mips64_flag : natural -> bool*) let is_pure_abi_cheri_mips64_flag flags:bool= (not (Nat_big_num.equal (Nat_big_num.bitwise_and flags ef_mips_abi_cheriabi)( (Nat_big_num.of_int 0)))) (*val is_valid_abi_cheri256_mips64_flag : natural -> bool*) let is_valid_abi_cheri256_mips64_flag flags:bool= (not (Nat_big_num.equal (Nat_big_num.bitwise_and flags ef_mips_mach_cheri256)( (Nat_big_num.of_int 0))))