69 open Hints_declaration
111 open StructuredTraces
115 val execute_1_preinstruction :
116 (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
117 BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
120 val execute_1_preinstruction_ok' :
121 (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
122 BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
123 Status.preStatus Types.sig0
125 val compute_target_of_unconditional_jump :
126 BitVector.word -> ASM.instruction -> BitVector.word
128 val is_unconditional_jump : ASM.instruction -> Bool.bool
130 val program_counter_after_other :
131 BitVector.word -> ASM.instruction -> BitVector.word
133 val addr_of_relative :
134 'a1 -> ASM.subaddressing_mode -> 'a1 Status.preStatus -> BitVector.word
137 BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
138 ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod ->
139 Status.status Types.sig0
141 val current_instruction_cost :
142 BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> Nat.nat
145 BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
146 Status.status Types.sig0
149 BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
152 val execute_1_pseudo_instruction0 :
153 (Nat.nat, Nat.nat) Types.prod -> ASM.pseudo_assembly_program ->
154 (ASM.identifier -> BitVector.word) -> (ASM.identifier -> BitVector.word) ->
155 Status.pseudoStatus -> ASM.pseudo_instruction -> BitVector.word ->
158 val execute_1_pseudo_instruction :
159 ASM.pseudo_assembly_program -> (BitVector.word -> __ -> (Nat.nat, Nat.nat)
160 Types.prod) -> (ASM.identifier -> BitVector.word) -> (ASM.identifier ->
161 BitVector.word) -> Status.pseudoStatus -> Status.pseudoStatus
164 Nat.nat -> BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->