19 open Hints_declaration
90 val jump_length_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
92 val jump_length_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
94 val jump_length_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
96 val jump_length_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
98 val jump_length_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
100 val jump_length_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
102 val jump_length_inv_rect_Type4 :
103 jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
105 val jump_length_inv_rect_Type3 :
106 jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
108 val jump_length_inv_rect_Type2 :
109 jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
111 val jump_length_inv_rect_Type1 :
112 jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
114 val jump_length_inv_rect_Type0 :
115 jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
117 val jump_length_discr : jump_length -> jump_length -> __
119 val jump_length_jmdiscr : jump_length -> jump_length -> __
121 val short_jump_cond :
122 BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
125 val absolute_jump_cond :
126 BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
129 val assembly_preinstruction :
130 ('a1 -> BitVector.byte) -> 'a1 ASM.preinstruction -> Bool.bool
131 Vector.vector List.list
133 val assembly1 : ASM.instruction -> Bool.bool Vector.vector List.list
135 val expand_relative_jump_internal :
136 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
137 (BitVector.word -> Bool.bool) -> ASM.identifier -> BitVector.word ->
138 (ASM.subaddressing_mode -> ASM.subaddressing_mode ASM.preinstruction) ->
139 ASM.instruction List.list
141 val expand_relative_jump :
142 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
143 (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.identifier
144 ASM.preinstruction -> ASM.instruction List.list
146 val is_code : AST.region -> Bool.bool
148 val expand_pseudo_instruction :
149 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
150 (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
151 (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
152 ASM.instruction List.list
154 val assembly_1_pseudoinstruction :
155 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
156 (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
157 (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
158 (Nat.nat, Bool.bool Vector.vector List.list) Types.prod
160 val instruction_size :
161 (ASM.identifier -> BitVector.word) -> (ASM.identifier -> (AST.region,
162 BitVector.word) Types.prod) -> (BitVector.word -> BitVector.word) ->
163 (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.pseudo_instruction
167 ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
168 (BitVector.word -> Bool.bool) -> ASM.labelled_object_code Types.sig0
170 val ticks_of_instruction : ASM.instruction -> Nat.nat
173 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
174 (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
175 BitVector.word -> ASM.pseudo_instruction -> (Nat.nat, Nat.nat) Types.prod
178 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
179 (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
180 BitVector.word -> (Nat.nat, Nat.nat) Types.prod