extracted/values.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 Coqlib
  30
  31 open ErrorMessages
  32
  33 open Option
  34
  35 open Setoids
  36
  37 open Monad
  38
  39 open Positive
  40
  41 open PreIdentifiers
  42
  43 open Errors
  44
  45 open Proper
  46
  47 open PositiveMap
  48
  49 open Deqsets
  50
  51 open Extralib
  52
  53 open Lists
  54
  55 open Identifiers
  56
  57 open Integers
  58
  59 open AST
  60
  61 open Division
  62
  63 open Exp
  64
  65 open Arithmetic
  66
  67 open Extranat
  68
  69 open Vector
  70
  71 open FoldStuff
  72
  73 open BitVector
  74
  75 open Z
  76
  77 open BitVectorZ
  78
  79 open Pointers
  80
  81 type val0 =
  82 | Vundef
  83 | Vint of AST.intsize * AST.bvint
  84 | Vnull
  85 | Vptr of Pointers.pointer
  86
  87 val val_rect_Type4 :
  88   'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
  89   'a1) -> val0 -> 'a1
  90
  91 val val_rect_Type5 :
  92   'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
  93   'a1) -> val0 -> 'a1
  94
  95 val val_rect_Type3 :
  96   'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
  97   'a1) -> val0 -> 'a1
  98
  99 val val_rect_Type2 :
 100   'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
 101   'a1) -> val0 -> 'a1
 102
 103 val val_rect_Type1 :
 104   'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
 105   'a1) -> val0 -> 'a1
 106
 107 val val_rect_Type0 :
 108   'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
 109   'a1) -> val0 -> 'a1
 110
 111 val val_inv_rect_Type4 :
 112   val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
 113   'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
 114
 115 val val_inv_rect_Type3 :
 116   val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
 117   'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
 118
 119 val val_inv_rect_Type2 :
 120   val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
 121   'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
 122
 123 val val_inv_rect_Type1 :
 124   val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
 125   'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
 126
 127 val val_inv_rect_Type0 :
 128   val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
 129   'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
 130
 131 val val_discr : val0 -> val0 -> __
 132
 133 val val_jmdiscr : val0 -> val0 -> __
 134
 135 val vzero : AST.intsize -> val0
 136
 137 val vone : AST.intsize -> val0
 138
 139 val mone : AST.intsize -> BitVector.bitVector
 140
 141 val vmone : AST.intsize -> val0
 142
 143 val vtrue : val0
 144
 145 val vfalse : val0
 146
 147 val of_bool : Bool.bool -> val0
 148
 149 val eval_bool_of_val : val0 -> Bool.bool Errors.res
 150
 151 val neg : val0 -> val0
 152
 153 val notint : val0 -> val0
 154
 155 val notbool : val0 -> val0
 156
 157 val zero_ext : AST.intsize -> val0 -> val0
 158
 159 val sign_ext : AST.intsize -> val0 -> val0
 160
 161 val add : val0 -> val0 -> val0
 162
 163 val sub : val0 -> val0 -> val0
 164
 165 val mul : val0 -> val0 -> val0
 166
 167 val v_and : val0 -> val0 -> val0
 168
 169 val or0 : val0 -> val0 -> val0
 170
 171 val xor : val0 -> val0 -> val0
 172
 173 val cmp_match : Integers.comparison -> val0
 174
 175 val cmp_mismatch : Integers.comparison -> val0
 176
 177 val cmp_offset :
 178   Integers.comparison -> Pointers.offset -> Pointers.offset -> Bool.bool
 179
 180 val cmp_int :
 181   Nat.nat -> Integers.comparison -> BitVector.bitVector ->
 182   BitVector.bitVector -> Bool.bool
 183
 184 val cmpu_int :
 185   Nat.nat -> Integers.comparison -> BitVector.bitVector ->
 186   BitVector.bitVector -> Bool.bool
 187
 188 val cmp : Integers.comparison -> val0 -> val0 -> val0
 189
 190 val cmpu : Integers.comparison -> val0 -> val0 -> val0
 191
 192 val load_result : AST.typ -> val0 -> val0
 193