extracted/semantics.mli

   1 open Preamble
   2
   3 open UtilBranch
   4
   5 open ASMCostsSplit
   6
   7 open StructuredTraces
   8
   9 open AbstractStatus
  10
  11 open StatusProofs
  12
  13 open Interpret
  14
  15 open ASMCosts
  16
  17 open Status
  18
  19 open Fetch
  20
  21 open Assembly
  22
  23 open PolicyFront
  24
  25 open PolicyStep
  26
  27 open Policy
  28
  29 open AssocList
  30
  31 open Uses
  32
  33 open ASM
  34
  35 open BitVectorTrieSet
  36
  37 open LINToASM
  38
  39 open LIN
  40
  41 open Linearise
  42
  43 open LTLToLIN
  44
  45 open Fixpoints
  46
  47 open Set_adt
  48
  49 open Liveness
  50
  51 open Interference
  52
  53 open Joint_LTL_LIN
  54
  55 open LTL
  56
  57 open ERTLToLTL
  58
  59 open ERTL
  60
  61 open RegisterSet
  62
  63 open RTLToERTL
  64
  65 open State
  66
  67 open Bind_new
  68
  69 open BindLists
  70
  71 open Blocks
  72
  73 open TranslateUtils
  74
  75 open String
  76
  77 open LabelledObjects
  78
  79 open I8051
  80
  81 open BackEndOps
  82
  83 open Joint
  84
  85 open RTL
  86
  87 open RTLabsToRTL
  88
  89 open CostInj
  90
  91 open Deqsets_extra
  92
  93 open CostMisc
  94
  95 open Listb_extra
  96
  97 open CostSpec
  98
  99 open CostCheck
 100
 101 open BitVectorTrie
 102
 103 open Graphs
 104
 105 open Order
 106
 107 open Registers
 108
 109 open RTLabs_syntax
 110
 111 open ToRTLabs
 112
 113 open FrontEndOps
 114
 115 open Cminor_syntax
 116
 117 open ToCminor
 118
 119 open MemProperties
 120
 121 open MemoryInjections
 122
 123 open Fresh
 124
 125 open SwitchRemoval
 126
 127 open Sets
 128
 129 open Listb
 130
 131 open Star
 132
 133 open Frontend_misc
 134
 135 open CexecInd
 136
 137 open Casts
 138
 139 open ClassifyOp
 140
 141 open Smallstep
 142
 143 open Extra_bool
 144
 145 open FrontEndVal
 146
 147 open Hide
 148
 149 open ByteValues
 150
 151 open GenMem
 152
 153 open FrontEndMem
 154
 155 open Globalenvs
 156
 157 open Csem
 158
 159 open SmallstepExec
 160
 161 open Division
 162
 163 open Z
 164
 165 open BitVectorZ
 166
 167 open Pointers
 168
 169 open Values
 170
 171 open Events
 172
 173 open IOMonad
 174
 175 open IO
 176
 177 open Cexec
 178
 179 open TypeComparison
 180
 181 open SimplifyCasts
 182
 183 open CostLabel
 184
 185 open Coqlib
 186
 187 open Proper
 188
 189 open PositiveMap
 190
 191 open Deqsets
 192
 193 open ErrorMessages
 194
 195 open PreIdentifiers
 196
 197 open Errors
 198
 199 open Extralib
 200
 201 open Lists
 202
 203 open Positive
 204
 205 open Identifiers
 206
 207 open Exp
 208
 209 open Arithmetic
 210
 211 open Vector
 212
 213 open Div_and_mod
 214
 215 open Util
 216
 217 open FoldStuff
 218
 219 open BitVector
 220
 221 open Jmeq
 222
 223 open Russell
 224
 225 open List
 226
 227 open Setoids
 228
 229 open Monad
 230
 231 open Option
 232
 233 open Extranat
 234
 235 open Bool
 236
 237 open Relations
 238
 239 open Nat
 240
 241 open Integers
 242
 243 open Hints_declaration
 244
 245 open Core_notation
 246
 247 open Pts
 248
 249 open Logic
 250
 251 open Types
 252
 253 open AST
 254
 255 open Csyntax
 256
 257 open Label
 258
 259 open Compiler
 260
 261 open Stacksize
 262
 263 open Executions
 264
 265 open Measurable
 266
 267 open Clight_abstract
 268
 269 open Clight_classified_system
 270
 271 open Cminor_semantics
 272
 273 open Cminor_abstract
 274
 275 open Cminor_classified_system
 276
 277 open RTLabs_semantics
 278
 279 open RTLabs_abstract
 280
 281 open RTLabs_classified_system
 282
 283 open ExtraMonads
 284
 285 open ExtraGlobalenvs
 286
 287 open I8051bis
 288
 289 open BEMem
 290
 291 open Joint_semantics
 292
 293 open SemanticsUtils
 294
 295 open Traces
 296
 297 open Joint_fullexec
 298
 299 open RTL_semantics
 300
 301 open ERTL_semantics
 302
 303 open Joint_LTL_LIN_semantics
 304
 305 open LTL_semantics
 306
 307 open LIN_semantics
 308
 309 open Interpret2
 310
 311 type preclassified_system_pass =
 312   Measurable.preclassified_system
 313   (* singleton inductive, whose constructor was mk_preclassified_system_pass *)
 314
 315 val preclassified_system_pass_rect_Type4 :
 316   Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
 317   preclassified_system_pass -> 'a1
 318
 319 val preclassified_system_pass_rect_Type5 :
 320   Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
 321   preclassified_system_pass -> 'a1
 322
 323 val preclassified_system_pass_rect_Type3 :
 324   Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
 325   preclassified_system_pass -> 'a1
 326
 327 val preclassified_system_pass_rect_Type2 :
 328   Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
 329   preclassified_system_pass -> 'a1
 330
 331 val preclassified_system_pass_rect_Type1 :
 332   Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
 333   preclassified_system_pass -> 'a1
 334
 335 val preclassified_system_pass_rect_Type0 :
 336   Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
 337   preclassified_system_pass -> 'a1
 338
 339 val pcs_pcs :
 340   Compiler.pass -> preclassified_system_pass ->
 341   Measurable.preclassified_system
 342
 343 val preclassified_system_pass_inv_rect_Type4 :
 344   Compiler.pass -> preclassified_system_pass ->
 345   (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
 346
 347 val preclassified_system_pass_inv_rect_Type3 :
 348   Compiler.pass -> preclassified_system_pass ->
 349   (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
 350
 351 val preclassified_system_pass_inv_rect_Type2 :
 352   Compiler.pass -> preclassified_system_pass ->
 353   (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
 354
 355 val preclassified_system_pass_inv_rect_Type1 :
 356   Compiler.pass -> preclassified_system_pass ->
 357   (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
 358
 359 val preclassified_system_pass_inv_rect_Type0 :
 360   Compiler.pass -> preclassified_system_pass ->
 361   (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
 362
 363 val pcs_pcs__o__pcs_exec :
 364   Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
 365   SmallstepExec.fullexec
 366
 367 val pcs_pcs__o__pcs_exec__o__es1 :
 368   Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
 369   SmallstepExec.trans_system
 370
 371 val preclassified_system_of_pass :
 372   Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass
 373
 374 val run_and_print :
 375   Compiler.pass -> Compiler.syntax_of_pass -> Nat.nat -> (Compiler.pass ->
 376   Types.unit0) -> (StructuredTraces.intensional_event -> Types.unit0) ->
 377   (Errors.errmsg -> Types.unit0) -> (Integers.int -> Types.unit0) ->
 378   Types.unit0
 379