extracted/abstractStatus.mli

   1 open Preamble
   2
   3 open Hide
   4
   5 open Integers
   6
   7 open AST
   8
   9 open Division
  10
  11 open Exp
  12
  13 open Arithmetic
  14
  15 open Extranat
  16
  17 open Vector
  18
  19 open FoldStuff
  20
  21 open BitVector
  22
  23 open Z
  24
  25 open BitVectorZ
  26
  27 open Pointers
  28
  29 open Coqlib
  30
  31 open Values
  32
  33 open Events
  34
  35 open IOMonad
  36
  37 open IO
  38
  39 open Sets
  40
  41 open Listb
  42
  43 open Proper
  44
  45 open PositiveMap
  46
  47 open Deqsets
  48
  49 open ErrorMessages
  50
  51 open PreIdentifiers
  52
  53 open Errors
  54
  55 open Extralib
  56
  57 open Setoids
  58
  59 open Monad
  60
  61 open Option
  62
  63 open Div_and_mod
  64
  65 open Russell
  66
  67 open Util
  68
  69 open List
  70
  71 open Lists
  72
  73 open Nat
  74
  75 open Positive
  76
  77 open Types
  78
  79 open Identifiers
  80
  81 open CostLabel
  82
  83 open Jmeq
  84
  85 open Hints_declaration
  86
  87 open Core_notation
  88
  89 open Pts
  90
  91 open Logic
  92
  93 open Relations
  94
  95 open Bool
  96
  97 open StructuredTraces
  98
  99 open BitVectorTrie
 100
 101 open String
 102
 103 open LabelledObjects
 104
 105 open ASM
 106
 107 open Status
 108
 109 open Fetch
 110
 111 val aSM_classify00 : 'a1 ASM.preinstruction -> StructuredTraces.status_class
 112
 113 val aSM_classify0 : ASM.instruction -> StructuredTraces.status_class
 114
 115 val current_instruction0 :
 116   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
 117   ASM.instruction
 118
 119 val current_instruction :
 120   BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
 121   ASM.instruction
 122
 123 val current_instruction_label :
 124   BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
 125   BitVectorTrie.bitVectorTrie -> Status.status -> CostLabel.costlabel
 126   Types.option
 127
 128 val word_deqset : Deqsets.deqSet
 129
 130 val oC_classify :
 131   BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
 132   StructuredTraces.status_class
 133