19 open Hints_declaration
88 (Nat.nat, (Nat.nat, Assembly.jump_length) Types.prod
89 BitVectorTrie.bitVectorTrie) Types.prod
91 val jmpeqb : Assembly.jump_length -> Assembly.jump_length -> Bool.bool
93 val expand_relative_jump_internal_unsafe :
94 Assembly.jump_length -> (ASM.subaddressing_mode -> ASM.subaddressing_mode
95 ASM.preinstruction) -> ASM.instruction List.list
98 ASM.identifier ASM.preinstruction -> (ASM.subaddressing_mode ->
99 ASM.subaddressing_mode ASM.preinstruction, ASM.instruction) Types.sum
101 val expand_relative_jump_unsafe :
102 Assembly.jump_length -> ASM.identifier ASM.preinstruction ->
103 ASM.instruction List.list
105 val expand_pseudo_instruction_unsafe :
106 Assembly.jump_length -> ASM.pseudo_instruction -> ASM.instruction List.list
108 val instruction_size_jmplen :
109 Assembly.jump_length -> ASM.pseudo_instruction -> Nat.nat
112 Assembly.jump_length -> Assembly.jump_length -> Assembly.jump_length
115 Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum
117 val dec_eq_jump_length :
118 Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum
120 val create_label_map :
121 ASM.labelled_instruction List.list -> Fetch.label_map Types.sig0
123 val select_reljump_length :
124 Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
125 Nat.nat -> Assembly.jump_length
127 val select_call_length :
128 Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
131 val select_jump_length :
132 Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
136 ASM.identifier ASM.preinstruction -> ASM.identifier Types.option
138 val length_of : ASM.identifier ASM.preinstruction -> Nat.nat
140 val jump_expansion_step_instruction :
141 Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
142 ASM.preinstruction -> Assembly.jump_length Types.option
144 val jump_expansion_start :
145 ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
146 ppc_pc_map Types.option Types.sig0