extracted/simplifyCasts.mli

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Coqlib
   6
   7 open Proper
   8
   9 open PositiveMap
  10
  11 open Deqsets
  12
  13 open ErrorMessages
  14
  15 open PreIdentifiers
  16
  17 open Errors
  18
  19 open Extralib
  20
  21 open Lists
  22
  23 open Positive
  24
  25 open Identifiers
  26
  27 open Exp
  28
  29 open Arithmetic
  30
  31 open Vector
  32
  33 open Div_and_mod
  34
  35 open Util
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Jmeq
  42
  43 open Russell
  44
  45 open List
  46
  47 open Setoids
  48
  49 open Monad
  50
  51 open Option
  52
  53 open Extranat
  54
  55 open Bool
  56
  57 open Relations
  58
  59 open Nat
  60
  61 open Integers
  62
  63 open Hints_declaration
  64
  65 open Core_notation
  66
  67 open Pts
  68
  69 open Logic
  70
  71 open Types
  72
  73 open AST
  74
  75 open Csyntax
  76
  77 open TypeComparison
  78
  79 open ClassifyOp
  80
  81 open Smallstep
  82
  83 open Extra_bool
  84
  85 open FrontEndVal
  86
  87 open Hide
  88
  89 open ByteValues
  90
  91 open GenMem
  92
  93 open FrontEndMem
  94
  95 open Globalenvs
  96
  97 open Csem
  98
  99 open SmallstepExec
 100
 101 open Division
 102
 103 open Z
 104
 105 open BitVectorZ
 106
 107 open Pointers
 108
 109 open Values
 110
 111 open Events
 112
 113 open IOMonad
 114
 115 open IO
 116
 117 open Cexec
 118
 119 open Casts
 120
 121 open CexecInd
 122
 123 open Sets
 124
 125 open Listb
 126
 127 open Star
 128
 129 open Frontend_misc
 130
 131 val reduce_bits :
 132   Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector ->
 133   BitVector.bitVector Types.option
 134
 135 val pred_bitsize_of_intsize : AST.intsize -> Nat.nat
 136
 137 val signed : AST.signedness -> Bool.bool
 138
 139 val simplify_int :
 140   AST.intsize -> AST.intsize -> AST.signedness -> AST.signedness -> AST.bvint
 141   -> AST.bvint Types.option
 142
 143 val size_lt_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum
 144
 145 val size_not_lt_to_ge : AST.intsize -> AST.intsize -> (__, __) Types.sum
 146
 147 val sign_eq_dect : AST.signedness -> AST.signedness -> (__, __) Types.sum
 148
 149 val necessary_conditions :
 150   AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> Bool.bool
 151
 152 val assert_int_value :
 153   Values.val0 Types.option -> AST.intsize -> BitVector.bitVector Types.option
 154
 155 val binop_simplifiable : Csyntax.binary_operation -> Bool.bool
 156
 157 val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0
 158
 159 val simplify_expr :
 160   Csyntax.expr -> AST.intsize -> AST.signedness -> (Bool.bool, Csyntax.expr)
 161   Types.prod Types.sig0
 162
 163 val simplify_e : Csyntax.expr -> Csyntax.expr
 164
 165 val simplify_ls : Csyntax.labeled_statements -> Csyntax.labeled_statements
 166
 167 val simplify_statement : Csyntax.statement -> Csyntax.statement
 168
 169 val simplify_function : Csyntax.function0 -> Csyntax.function0
 170
 171 val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef
 172
 173 val simplify_program : Csyntax.clight_program -> Csyntax.clight_program
 174