extracted/switchRemoval.mli

   1 open Preamble
   2
   3 open Deqsets
   4
   5 open Sets
   6
   7 open Bool
   8
   9 open Relations
  10
  11 open Nat
  12
  13 open Hints_declaration
  14
  15 open Core_notation
  16
  17 open Pts
  18
  19 open Logic
  20
  21 open Types
  22
  23 open List
  24
  25 open Listb
  26
  27 open Proper
  28
  29 open PositiveMap
  30
  31 open ErrorMessages
  32
  33 open PreIdentifiers
  34
  35 open Errors
  36
  37 open Extralib
  38
  39 open Setoids
  40
  41 open Monad
  42
  43 open Option
  44
  45 open Div_and_mod
  46
  47 open Jmeq
  48
  49 open Russell
  50
  51 open Util
  52
  53 open Lists
  54
  55 open Positive
  56
  57 open Identifiers
  58
  59 open CostLabel
  60
  61 open Coqlib
  62
  63 open Exp
  64
  65 open Arithmetic
  66
  67 open Vector
  68
  69 open FoldStuff
  70
  71 open BitVector
  72
  73 open Extranat
  74
  75 open Integers
  76
  77 open AST
  78
  79 open Csyntax
  80
  81 open Fresh
  82
  83 open CexecInd
  84
  85 open SmallstepExec
  86
  87 open Cexec
  88
  89 open IO
  90
  91 open IOMonad
  92
  93 open Star
  94
  95 open ClassifyOp
  96
  97 open Events
  98
  99 open Smallstep
 100
 101 open Extra_bool
 102
 103 open Values
 104
 105 open FrontEndVal
 106
 107 open Hide
 108
 109 open ByteValues
 110
 111 open Division
 112
 113 open Z
 114
 115 open BitVectorZ
 116
 117 open Pointers
 118
 119 open GenMem
 120
 121 open FrontEndMem
 122
 123 open Globalenvs
 124
 125 open Csem
 126
 127 open TypeComparison
 128
 129 open Frontend_misc
 130
 131 open MemProperties
 132
 133 open MemoryInjections
 134
 135 val convert_break_to_goto :
 136   Csyntax.statement -> Csyntax.label -> Csyntax.statement
 137
 138 val produce_cond :
 139   Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
 140   Csyntax.label -> ((Csyntax.statement, Csyntax.label) Types.prod,
 141   Identifiers.universe) Types.prod
 142
 143 val simplify_switch :
 144   Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
 145   (Csyntax.statement, Identifiers.universe) Types.prod
 146
 147 val switch_removal_branches :
 148   Csyntax.labeled_statements -> Identifiers.universe ->
 149   ((Csyntax.labeled_statements, (AST.ident, Csyntax.type0) Types.prod
 150   List.list) Types.prod, Identifiers.universe) Types.prod
 151
 152 val switch_removal :
 153   Csyntax.statement -> Identifiers.universe -> ((Csyntax.statement,
 154   (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
 155   Identifiers.universe) Types.prod
 156
 157 val ret_st :
 158   (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
 159   Identifiers.universe) Types.prod -> 'a1
 160
 161 val ret_vars :
 162   (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
 163   Identifiers.universe) Types.prod -> (AST.ident, Csyntax.type0) Types.prod
 164   List.list
 165
 166 val ret_u :
 167   (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
 168   Identifiers.universe) Types.prod -> Identifiers.universe
 169
 170 val least_identifier : PreIdentifiers.identifier
 171
 172 val max_of_expr : Csyntax.expr -> AST.ident
 173
 174 val max_of_ls : Csyntax.labeled_statements -> AST.ident
 175
 176 val max_of_statement : Csyntax.statement -> AST.ident
 177
 178 val max_id_of_function : Csyntax.function0 -> AST.ident
 179
 180 val function_switch_removal :
 181   Csyntax.function0 -> (Csyntax.function0, (AST.ident, Csyntax.type0)
 182   Types.prod List.list) Types.prod
 183
 184 val fundef_switch_removal : Csyntax.clight_fundef -> Csyntax.clight_fundef
 185
 186 val program_switch_removal : Csyntax.clight_program -> Csyntax.clight_program
 187
 188 val nonempty_block_rect_Type4 :
 189   GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
 190
 191 val nonempty_block_rect_Type5 :
 192   GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
 193
 194 val nonempty_block_rect_Type3 :
 195   GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
 196
 197 val nonempty_block_rect_Type2 :
 198   GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
 199
 200 val nonempty_block_rect_Type1 :
 201   GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
 202
 203 val nonempty_block_rect_Type0 :
 204   GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
 205
 206 val nonempty_block_inv_rect_Type4 :
 207   GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
 208
 209 val nonempty_block_inv_rect_Type3 :
 210   GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
 211
 212 val nonempty_block_inv_rect_Type2 :
 213   GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
 214
 215 val nonempty_block_inv_rect_Type1 :
 216   GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
 217
 218 val nonempty_block_inv_rect_Type0 :
 219   GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
 220
 221 val nonempty_block_discr : GenMem.mem -> Pointers.block -> __
 222
 223 val nonempty_block_jmdiscr : GenMem.mem -> Pointers.block -> __
 224
 225 val sr_memext_rect_Type4 :
 226   GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
 227   'a1) -> 'a1
 228
 229 val sr_memext_rect_Type5 :
 230   GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
 231   'a1) -> 'a1
 232
 233 val sr_memext_rect_Type3 :
 234   GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
 235   'a1) -> 'a1
 236
 237 val sr_memext_rect_Type2 :
 238   GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
 239   'a1) -> 'a1
 240
 241 val sr_memext_rect_Type1 :
 242   GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
 243   'a1) -> 'a1
 244
 245 val sr_memext_rect_Type0 :
 246   GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
 247   'a1) -> 'a1
 248
 249 val sr_memext_inv_rect_Type4 :
 250   GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
 251   __ -> 'a1) -> 'a1
 252
 253 val sr_memext_inv_rect_Type3 :
 254   GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
 255   __ -> 'a1) -> 'a1
 256
 257 val sr_memext_inv_rect_Type2 :
 258   GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
 259   __ -> 'a1) -> 'a1
 260
 261 val sr_memext_inv_rect_Type1 :
 262   GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
 263   __ -> 'a1) -> 'a1
 264
 265 val sr_memext_inv_rect_Type0 :
 266   GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
 267   __ -> 'a1) -> 'a1
 268
 269 val sr_memext_discr :
 270   GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __
 271
 272 val sr_memext_jmdiscr :
 273   GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __
 274
 275 val env_codomain :
 276   Csem.env -> (AST.ident, Csyntax.type0) Types.prod List.list ->
 277   Pointers.block Frontend_misc.lset
 278