99 open Hints_declaration
117 val aSMRegisterRets : ASM.subaddressing_mode List.list
119 val as_result_of_finaladdr :
120 'a1 -> 'a1 Status.preStatus -> BitVector.word -> Integers.int Types.option
122 val oC_as_call_ident :
123 ASM.labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie ->
124 Status.status Types.sig0 -> AST.ident
126 val oC_abstract_status :
127 ASM.labelled_object_code -> StructuredTraces.abstract_status
129 val trace_any_label_length :
130 ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
131 Status.status -> Status.status -> StructuredTraces.trace_any_label ->
134 val all_program_counter_list : Nat.nat -> BitVector.bitVector List.list
136 val compute_paid_trace_any_label :
137 ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
138 Status.status -> Status.status -> StructuredTraces.trace_any_label ->
141 val compute_paid_trace_label_label :
142 ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
143 Status.status -> Status.status -> StructuredTraces.trace_label_label ->
147 ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Bool.bool ->
151 ASM.labelled_object_code -> BitVector.word -> Nat.nat Types.sig0