extracted/cminor_abstract.mli

   1 open Preamble
   2
   3 open FrontEndOps
   4
   5 open Cminor_syntax
   6
   7 open SmallstepExec
   8
   9 open Extra_bool
  10
  11 open Globalenvs
  12
  13 open IOMonad
  14
  15 open IO
  16
  17 open FrontEndVal
  18
  19 open Hide
  20
  21 open ByteValues
  22
  23 open GenMem
  24
  25 open FrontEndMem
  26
  27 open CostLabel
  28
  29 open Proper
  30
  31 open PositiveMap
  32
  33 open Deqsets
  34
  35 open Extralib
  36
  37 open Lists
  38
  39 open Identifiers
  40
  41 open Integers
  42
  43 open AST
  44
  45 open Division
  46
  47 open Exp
  48
  49 open Arithmetic
  50
  51 open Extranat
  52
  53 open Vector
  54
  55 open FoldStuff
  56
  57 open BitVector
  58
  59 open Z
  60
  61 open BitVectorZ
  62
  63 open Pointers
  64
  65 open ErrorMessages
  66
  67 open Option
  68
  69 open Setoids
  70
  71 open Monad
  72
  73 open Positive
  74
  75 open PreIdentifiers
  76
  77 open Errors
  78
  79 open Div_and_mod
  80
  81 open Jmeq
  82
  83 open Russell
  84
  85 open Util
  86
  87 open Bool
  88
  89 open Relations
  90
  91 open Nat
  92
  93 open List
  94
  95 open Hints_declaration
  96
  97 open Core_notation
  98
  99 open Pts
 100
 101 open Logic
 102
 103 open Types
 104
 105 open Coqlib
 106
 107 open Values
 108
 109 open Events
 110
 111 open Cminor_semantics
 112
 113 type cminor_state = Cminor_semantics.state
 114
 115 val cminor_labelled : Cminor_semantics.state -> Bool.bool
 116
 117 open Sets
 118
 119 open Listb
 120
 121 open StructuredTraces
 122
 123 val cminor_classify : Cminor_semantics.state -> StructuredTraces.status_class
 124
 125 type cm_genv = Cminor_semantics.genv
 126
 127 type cm_env = Cminor_semantics.env
 128
 129 type cm_cont = Cminor_semantics.cont
 130
 131 val cm_eval_expr :
 132   Cminor_semantics.genv -> AST.typ -> Cminor_syntax.expr ->
 133   Cminor_semantics.env -> Pointers.block -> GenMem.mem -> (Events.trace,
 134   Values.val0) Types.prod Errors.res
 135
 136 val cmState :
 137   Cminor_syntax.internal_function -> Cminor_syntax.stmt ->
 138   Cminor_semantics.env -> GenMem.mem -> Pointers.block ->
 139   Cminor_semantics.cont -> Cminor_semantics.stack -> Cminor_semantics.state
 140
 141 val cmReturnstate :
 142   Values.val0 Types.option -> GenMem.mem -> Cminor_semantics.stack ->
 143   Cminor_semantics.state
 144
 145 val cmCallstate :
 146   AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 147   List.list -> GenMem.mem -> Cminor_semantics.stack -> Cminor_semantics.state
 148