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/gnu_ext_program_header_table.ml.html

Source file gnu_ext_program_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
26
27
28
29
30
31
32
33
34
(*Generated by Lem from gnu_extensions/gnu_ext_program_header_table.lem.*)
(** [gnu_ext_program_header_table] contains GNU extension specific functionality
  * related to the program header table.
  *)

open Lem_basic_classes
open Lem_num

(** GNU extensions, as defined in the LSB, see section 11.2. *)

(** The element specifies the location and size of a segment that may be made
  * read-only after relocations have been processed.
  *)
let elf_pt_gnu_relro : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 4))( (Nat_big_num.of_int 421345620)))( (Nat_big_num.of_int 2))) (* 0x6474e552 *)
(** The [p_flags] member specifies the permissions of the segment containing the
  * stack and is used to indicate whether the stack should be executable.
  *)
let elf_pt_gnu_stack : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 4))( (Nat_big_num.of_int 421345620)))( (Nat_big_num.of_int 1))) (* 0x6474e551 *)
(** Element specifies the location and size of exception handling information. *)
let elf_pt_gnu_eh_frame : Nat_big_num.num=  (Nat_big_num.mul( (Nat_big_num.of_int 4))( (Nat_big_num.of_int 421345620)))    (* 0x6474e550 *)

(** [string_of_gnu_ext_segment_type m] produces a string representation of
  * GNU extension segment type [m].
  *)
(*val string_of_gnu_ext_segment_type : natural -> string*)
let string_of_gnu_ext_segment_type pt:string=
   (if Nat_big_num.equal pt elf_pt_gnu_relro then
    "GNU_RELRO"
  else if Nat_big_num.equal pt elf_pt_gnu_stack then
    "GNU_STACK"
  else if Nat_big_num.equal pt elf_pt_gnu_eh_frame then
    "GNU_EH_FRAME"
  else
    "Invalid GNU EXT segment type")
OCaml

Innovation. Community. Security.