extracted/aSMCostsSplit.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 UtilBranch
 120
 121 val traverse_code_internal :
 122   ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Nat.nat
 123   Identifiers.identifier_map Types.sig0
 124
 125 val traverse_code :
 126   ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0
 127
 128 val compute_costs :
 129   ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0
 130
 131 val aSM_cost_map : ASM.labelled_object_code -> StructuredTraces.as_cost_map
 132