99 open Hints_declaration
127 val mk_trans_system_of_abstract_status :
128 StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
129 (IO.io_out, IO.io_in) SmallstepExec.trans_system
131 val mk_fullexec_of_abstract_status :
132 StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
133 __ -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
135 val mk_preclassified_system_of_abstract_status :
136 StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
137 __ -> Measurable.preclassified_system
139 val oC_preclassified_system :
140 ASM.labelled_object_code -> Measurable.preclassified_system
144 val execute_1_pseudo_instruction' :
145 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
146 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
147 (BitVector.word -> Bool.bool) -> Status.pseudoStatus -> Status.pseudoStatus
149 val classify_pseudo_instruction :
150 ASM.pseudo_instruction -> StructuredTraces.status_class
153 ASM.pseudo_assembly_program -> Status.pseudoStatus ->
154 StructuredTraces.status_class
156 val aSM_as_label_of_pc :
157 ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
161 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
162 Status.pseudoStatus -> Integers.int Types.option
166 val aSM_as_call_ident :
167 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
168 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
169 (BitVector.word -> Bool.bool) -> Status.pseudoStatus Types.sig0 ->
172 val aSM_abstract_status :
173 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
174 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
175 (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status
177 val aSM_preclassified_system :
178 ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
179 (BitVector.word -> Bool.bool) -> Measurable.preclassified_system
182 ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
183 (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status