Source file `abi_power64_dynamic.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
(*Generated by Lem from abis/power64/abi_power64_dynamic.lem.*)
open Lem_basic_classes
open Lem_num
open Lem_string

open Error
open Show
open String_table

open Elf_dynamic
open Elf_types_native_uint

let abi_power64_dt_ppcgot : Nat_big_num.num=  ( Nat_big_num.mul( (Nat_big_num.of_int 939524096))( (Nat_big_num.of_int 2))) (* 0x70000000 *)

(*val string_of_abi_power64_dynamic_tag : natural -> string*)
let string_of_abi_power64_dynamic_tag m:string=
   (if Nat_big_num.equal m abi_power64_dt_ppcgot then
    "PPC64_GLINK"
  else
    "Invalid Power64 dynamic tag")

(*val abi_power64_tag_correspondence_of_tag : natural -> error tag_correspondence*)
let abi_power64_tag_correspondence_of_tag m:(tag_correspondence)error=
   (if Nat_big_num.equal m abi_power64_dt_ppcgot then
    return C_Ptr
  else
    fail ("abi_power64_tag_correspondence_of_tag: invalid Power64 dynamic tag"))
    
(*val abi_power64_elf64_value_of_elf64_dyn : elf64_dyn -> string_table -> error elf64_dyn_value*)
let abi_power64_elf64_value_of_elf64_dyn dyn stbl:(((Uint64_wrapper.uint64),(Uint64_wrapper.uint64))dyn_value)error=
   (let tag = (Nat_big_num.abs (Nat_big_num.of_int64 dyn.elf64_dyn_tag)) in
    if Nat_big_num.equal tag abi_power64_dt_ppcgot then bind (match dyn.elf64_dyn_d_un with
        | D_Val     v -> fail "abi_power64_elf64_value_of_elf64_dyn: PPC_GOT must be a PTR"
        | D_Ptr     p -> return p
        | D_Ignored i -> fail "abi_power64_elf64_value_of_elf64_dyn: PPC_GOT must be a PTR"
      ) (fun addr ->
      return (Address addr))
    else
      fail ("abi_power64_elf64_value_of_elf64_dyn: invalid Power64 dynamic tag"))