extracted/cexec.mli

   1 open Preamble
   2
   3 open Div_and_mod
   4
   5 open Jmeq
   6
   7 open Russell
   8
   9 open Util
  10
  11 open Bool
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open List
  18
  19 open Hints_declaration
  20
  21 open Core_notation
  22
  23 open Pts
  24
  25 open Logic
  26
  27 open Types
  28
  29 open Extralib
  30
  31 open CostLabel
  32
  33 open PositiveMap
  34
  35 open Deqsets
  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 Coqlib
  66
  67 open Values
  68
  69 open Events
  70
  71 open Proper
  72
  73 open ErrorMessages
  74
  75 open Option
  76
  77 open Setoids
  78
  79 open Monad
  80
  81 open Positive
  82
  83 open PreIdentifiers
  84
  85 open Errors
  86
  87 open IOMonad
  88
  89 open IO
  90
  91 open SmallstepExec
  92
  93 open TypeComparison
  94
  95 open ClassifyOp
  96
  97 open Smallstep
  98
  99 open Csyntax
 100
 101 open Extra_bool
 102
 103 open FrontEndVal
 104
 105 open Hide
 106
 107 open ByteValues
 108
 109 open GenMem
 110
 111 open FrontEndMem
 112
 113 open Globalenvs
 114
 115 open Csem
 116
 117 val exec_bool_of_val : Values.val0 -> Csyntax.type0 -> Bool.bool Errors.res
 118
 119 val try_cast_null :
 120   GenMem.mem -> AST.intsize -> BitVector.bitVector -> Csyntax.type0 ->
 121   Csyntax.type0 -> Values.val0 Errors.res
 122
 123 val ptr_like_type : Csyntax.type0 -> Bool.bool
 124
 125 val exec_cast :
 126   GenMem.mem -> Values.val0 -> Csyntax.type0 -> Csyntax.type0 -> Values.val0
 127   Errors.res
 128
 129 val load_value_of_type' :
 130   Csyntax.type0 -> GenMem.mem -> (Pointers.block, Pointers.offset) Types.prod
 131   -> Values.val0 Types.option
 132
 133 val exec_lvalue :
 134   Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr -> ((Pointers.block,
 135   Pointers.offset) Types.prod, Events.trace) Types.prod Errors.res
 136
 137 val exec_lvalue' :
 138   Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr_descr -> Csyntax.type0
 139   -> ((Pointers.block, Pointers.offset) Types.prod, Events.trace) Types.prod
 140   Errors.res
 141
 142 val exec_expr :
 143   Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr -> (Values.val0,
 144   Events.trace) Types.prod Errors.res
 145
 146 val exec_exprlist :
 147   Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr List.list ->
 148   (Values.val0 List.list, Events.trace) Types.prod Errors.res
 149
 150 val exec_alloc_variables :
 151   Csem.env -> GenMem.mem -> (AST.ident, Csyntax.type0) Types.prod List.list
 152   -> (Csem.env, GenMem.mem) Types.prod
 153
 154 val exec_bind_parameters :
 155   Csem.env -> GenMem.mem -> (AST.ident, Csyntax.type0) Types.prod List.list
 156   -> Values.val0 List.list -> GenMem.mem Errors.res
 157
 158 val is_is_call_cont : Csem.cont -> (__, __) Types.sum
 159
 160 val is_Sskip : Csyntax.statement -> (__, __) Types.sum
 161
 162 val store_value_of_type' :
 163   Csyntax.type0 -> GenMem.mem -> (Pointers.block, Pointers.offset) Types.prod
 164   -> Values.val0 -> GenMem.mem Types.option
 165
 166 val exec_step :
 167   Csem.genv -> Csem.state -> (IO.io_out, IO.io_in, (Events.trace, Csem.state)
 168   Types.prod) IOMonad.iO
 169
 170 val make_global : Csyntax.clight_program -> Csem.genv
 171
 172 val make_initial_state : Csyntax.clight_program -> Csem.state Errors.res
 173
 174 val is_final : Csem.state -> Integers.int Types.option
 175
 176 val is_final_state : Csem.state -> (Integers.int Types.sig0, __) Types.sum
 177
 178 val exec_steps :
 179   Nat.nat -> Csem.genv -> Csem.state -> (IO.io_out, IO.io_in, (Events.trace,
 180   Csem.state) Types.prod) IOMonad.iO
 181
 182 val clight_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
 183
 184 val clight_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
 185