109 open Hints_declaration
129 (** val zoo : Pointers.offset -> Z.z **)
131 BitVectorZ.z_of_unsigned_bitvector Pointers.offset_size (Pointers.offv x)
133 (** val boo : Z.z -> Pointers.offset **)
135 BitVectorZ.bitvector_of_Z Pointers.offset_size x
137 (** val block_decidable_eq :
138 Pointers.block -> Pointers.block -> (__, __) Types.sum **)
139 let block_decidable_eq clearme =
143 (match Z.decidable_eq_Z_Type a b with
144 | Types.Inl _ -> Types.Inl __
145 | Types.Inr _ -> Types.Inr __))
148 Pointers.block -> (Pointers.block, Pointers.offset) Types.prod Types.option
150 (** val offset_plus :
151 Pointers.offset -> Pointers.offset -> Pointers.offset **)
152 let offset_plus o1 o2 =
153 Arithmetic.addition_n Pointers.offset_size (Pointers.offv o1)
156 (** val pointer_translation :
157 Pointers.pointer -> embedding -> Pointers.pointer Types.option **)
158 let pointer_translation p e =
159 let { Pointers.pblock = pblock; Pointers.poff = poff } = p in
161 | Types.None -> Types.None
163 let { Types.fst = dest_block; Types.snd = dest_off } = loc in
164 let ptr = { Pointers.pblock = dest_block; Pointers.poff =
165 (offset_plus poff dest_off) }
169 (** val memory_inj_rect_Type4 :
170 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
171 __ -> __ -> 'a1) -> 'a1 **)
172 let rec memory_inj_rect_Type4 e m1 m2 h_mk_memory_inj =
173 h_mk_memory_inj __ __ __ __ __ __ __
175 (** val memory_inj_rect_Type5 :
176 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
177 __ -> __ -> 'a1) -> 'a1 **)
178 let rec memory_inj_rect_Type5 e m1 m2 h_mk_memory_inj =
179 h_mk_memory_inj __ __ __ __ __ __ __
181 (** val memory_inj_rect_Type3 :
182 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
183 __ -> __ -> 'a1) -> 'a1 **)
184 let rec memory_inj_rect_Type3 e m1 m2 h_mk_memory_inj =
185 h_mk_memory_inj __ __ __ __ __ __ __
187 (** val memory_inj_rect_Type2 :
188 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
189 __ -> __ -> 'a1) -> 'a1 **)
190 let rec memory_inj_rect_Type2 e m1 m2 h_mk_memory_inj =
191 h_mk_memory_inj __ __ __ __ __ __ __
193 (** val memory_inj_rect_Type1 :
194 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
195 __ -> __ -> 'a1) -> 'a1 **)
196 let rec memory_inj_rect_Type1 e m1 m2 h_mk_memory_inj =
197 h_mk_memory_inj __ __ __ __ __ __ __
199 (** val memory_inj_rect_Type0 :
200 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
201 __ -> __ -> 'a1) -> 'a1 **)
202 let rec memory_inj_rect_Type0 e m1 m2 h_mk_memory_inj =
203 h_mk_memory_inj __ __ __ __ __ __ __
205 (** val memory_inj_inv_rect_Type4 :
206 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
207 __ -> __ -> __ -> 'a1) -> 'a1 **)
208 let memory_inj_inv_rect_Type4 x1 x2 x3 h1 =
209 let hcut = memory_inj_rect_Type4 x1 x2 x3 h1 in hcut __
211 (** val memory_inj_inv_rect_Type3 :
212 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
213 __ -> __ -> __ -> 'a1) -> 'a1 **)
214 let memory_inj_inv_rect_Type3 x1 x2 x3 h1 =
215 let hcut = memory_inj_rect_Type3 x1 x2 x3 h1 in hcut __
217 (** val memory_inj_inv_rect_Type2 :
218 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
219 __ -> __ -> __ -> 'a1) -> 'a1 **)
220 let memory_inj_inv_rect_Type2 x1 x2 x3 h1 =
221 let hcut = memory_inj_rect_Type2 x1 x2 x3 h1 in hcut __
223 (** val memory_inj_inv_rect_Type1 :
224 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
225 __ -> __ -> __ -> 'a1) -> 'a1 **)
226 let memory_inj_inv_rect_Type1 x1 x2 x3 h1 =
227 let hcut = memory_inj_rect_Type1 x1 x2 x3 h1 in hcut __
229 (** val memory_inj_inv_rect_Type0 :
230 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
231 __ -> __ -> __ -> 'a1) -> 'a1 **)
232 let memory_inj_inv_rect_Type0 x1 x2 x3 h1 =
233 let hcut = memory_inj_rect_Type0 x1 x2 x3 h1 in hcut __
235 (** val memory_inj_jmdiscr : embedding -> GenMem.mem -> GenMem.mem -> __ **)
236 let memory_inj_jmdiscr a1 a2 a3 =
237 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) __
239 (** val typesize' : Csyntax.type0 -> Nat.nat **)
241 AST.typesize (Csyntax.typ_of_type ty)