extracted/interpret2.mli

   1 open Preamble
   2
   3 open Fetch
   4
   5 open Hide
   6
   7 open Division
   8
   9 open Z
  10
  11 open BitVectorZ
  12
  13 open Pointers
  14
  15 open Coqlib
  16
  17 open Values
  18
  19 open Events
  20
  21 open IOMonad
  22
  23 open IO
  24
  25 open Sets
  26
  27 open Listb
  28
  29 open StructuredTraces
  30
  31 open AbstractStatus
  32
  33 open BitVectorTrie
  34
  35 open String
  36
  37 open Exp
  38
  39 open Arithmetic
  40
  41 open Vector
  42
  43 open FoldStuff
  44
  45 open BitVector
  46
  47 open Extranat
  48
  49 open Integers
  50
  51 open AST
  52
  53 open LabelledObjects
  54
  55 open Proper
  56
  57 open PositiveMap
  58
  59 open Deqsets
  60
  61 open ErrorMessages
  62
  63 open PreIdentifiers
  64
  65 open Errors
  66
  67 open Extralib
  68
  69 open Setoids
  70
  71 open Monad
  72
  73 open Option
  74
  75 open Div_and_mod
  76
  77 open Util
  78
  79 open List
  80
  81 open Lists
  82
  83 open Bool
  84
  85 open Relations
  86
  87 open Nat
  88
  89 open Positive
  90
  91 open Identifiers
  92
  93 open CostLabel
  94
  95 open ASM
  96
  97 open Types
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Jmeq
 108
 109 open Russell
 110
 111 open Status
 112
 113 open StatusProofs
 114
 115 open Interpret
 116
 117 open ASMCosts
 118
 119 open Stacksize
 120
 121 open SmallstepExec
 122
 123 open Executions
 124
 125 open Measurable
 126
 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
 130
 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
 134
 135 val mk_preclassified_system_of_abstract_status :
 136   StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
 137   __ -> Measurable.preclassified_system
 138
 139 val oC_preclassified_system :
 140   ASM.labelled_object_code -> Measurable.preclassified_system
 141
 142 open Assembly
 143
 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
 148
 149 val classify_pseudo_instruction :
 150   ASM.pseudo_instruction -> StructuredTraces.status_class
 151
 152 val aSM_classify :
 153   ASM.pseudo_assembly_program -> Status.pseudoStatus ->
 154   StructuredTraces.status_class
 155
 156 val aSM_as_label_of_pc :
 157   ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
 158   Types.option
 159
 160 val aSM_as_result :
 161   ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
 162   Status.pseudoStatus -> Integers.int Types.option
 163
 164 open AssocList
 165
 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 ->
 170   AST.ident
 171
 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
 176
 177 val aSM_preclassified_system :
 178   ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
 179   (BitVector.word -> Bool.bool) -> Measurable.preclassified_system
 180