package linksem

  1. Overview
  2. Docs
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_aarch64_section_header_table.ml.html

Source file abi_aarch64_section_header_table.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
(*Generated by Lem from abis/aarch64/abi_aarch64_section_header_table.lem.*)
(** [abi_aarch64_section_header_table], AARCH64 ABI specific definitions related
  * to the section header table.
  *)

open Lem_basic_classes
open Lem_num

(** AARCH64 specific section types *)

(** Contains build attributes.  What these are is not specified, and compilers
  * are free to insert their own proprietary information in this section.  See
  * Section 4.3.
  *)
let sht_aarch64_attributes : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 939524097))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1))) (* 0x70000003 *)

(** [string_of_aarch64_section_type m] produces a string based representation of
  * AARCH64 section type [m].
  *)
(*val string_of_aarch64_section_type : natural -> string*)
let string_of_aarch64_section_type m:string=
   (if Nat_big_num.equal m sht_aarch64_attributes then
    ".ARM.attributes"
  else
    "Unrecognised section type")
OCaml

Innovation. Community. Security.