open Preamble

open Hide

open Integers

open AST

open Division

open Exp

open Arithmetic

open Extranat

open Vector

open FoldStuff

open BitVector

open Z

open BitVectorZ

open Pointers

open Coqlib

open Values

open Events

open IOMonad

open IO

open Sets

open Listb

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Div_and_mod

open Russell

open Util

open List

open Lists

open Nat

open Positive

open Types

open Identifiers

open CostLabel

open Jmeq

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

open Bool

open StructuredTraces

open BitVectorTrie

open String

open LabelledObjects

open ASM

open Status

open Fetch

val aSM_classify00 : 'a1 ASM.preinstruction -> StructuredTraces.status_class

val aSM_classify0 : ASM.instruction -> StructuredTraces.status_class

val current_instruction :
  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
  ASM.instruction

val current_instruction_label :
  BitVector.byte BitVectorTrie.bitVectorTrie -> ASM.costlabel_map ->
  Status.status -> CostLabel.costlabel Types.option

val word_deqset : Deqsets.deqSet

val oC_classify :
  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
  StructuredTraces.status_class