source: extracted/memoryInjections.ml @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 7 years ago

...

File size: 5.1 KB
Line 
1open Preamble
2
3open TypeComparison
4
5open ClassifyOp
6
7open Smallstep
8
9open Csyntax
10
11open Extra_bool
12
13open FrontEndVal
14
15open Hide
16
17open ByteValues
18
19open GenMem
20
21open FrontEndMem
22
23open Globalenvs
24
25open Csem
26
27open SmallstepExec
28
29open CostLabel
30
31open PositiveMap
32
33open Deqsets
34
35open Lists
36
37open Identifiers
38
39open Integers
40
41open AST
42
43open Division
44
45open Arithmetic
46
47open Extranat
48
49open Vector
50
51open FoldStuff
52
53open BitVector
54
55open Z
56
57open BitVectorZ
58
59open Pointers
60
61open Coqlib
62
63open Values
64
65open Events
66
67open Proper
68
69open ErrorMessages
70
71open Option
72
73open Setoids
74
75open Monad
76
77open Positive
78
79open PreIdentifiers
80
81open Errors
82
83open IOMonad
84
85open IO
86
87open Div_and_mod
88
89open Jmeq
90
91open Russell
92
93open Util
94
95open Bool
96
97open Relations
98
99open Nat
100
101open List
102
103open Hints_declaration
104
105open Core_notation
106
107open Pts
108
109open Logic
110
111open Types
112
113open Extralib
114
115open Cexec
116
117open Sets
118
119open Listb
120
121open Star
122
123open Frontend_misc
124
125open MemProperties
126
127(** val zoo : Pointers.offset -> Z.z **)
128let zoo x =
129  BitVectorZ.z_of_unsigned_bitvector Pointers.offset_size (Pointers.offv x)
130
131(** val boo : Z.z -> Pointers.offset **)
132let boo x =
133  BitVectorZ.bitvector_of_Z Pointers.offset_size x
134
135(** val block_decidable_eq :
136    Pointers.block -> Pointers.block -> (__, __) Types.sum **)
137let block_decidable_eq clearme =
138  let a = clearme in
139  (fun clearme0 ->
140  let b = clearme0 in
141  (match Z.decidable_eq_Z_Type a b with
142   | Types.Inl _ -> Types.Inl __
143   | Types.Inr _ -> Types.Inr __))
144
145type embedding =
146  Pointers.block -> (Pointers.block, Pointers.offset) Types.prod Types.option
147
148(** val offset_plus :
149    Pointers.offset -> Pointers.offset -> Pointers.offset **)
150let offset_plus o1 o2 =
151  Arithmetic.addition_n Pointers.offset_size (Pointers.offv o1)
152    (Pointers.offv o2)
153
154(** val pointer_translation :
155    Pointers.pointer -> embedding -> Pointers.pointer Types.option **)
156let pointer_translation p e1 =
157  let { Pointers.pblock = pblock0; Pointers.poff = poff0 } = p in
158  (match e1 pblock0 with
159   | Types.None -> Types.None
160   | Types.Some loc ->
161     let { Types.fst = dest_block; Types.snd = dest_off } = loc in
162     let ptr = { Pointers.pblock = dest_block; Pointers.poff =
163       (offset_plus poff0 dest_off) }
164     in
165     Types.Some ptr)
166
167(** val memory_inj_rect_Type4 :
168    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
169    __ -> __ -> 'a1) -> 'a1 **)
170let rec memory_inj_rect_Type4 e1 m1 m2 h_mk_memory_inj =
171  h_mk_memory_inj __ __ __ __ __ __ __
172
173(** val memory_inj_rect_Type5 :
174    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
175    __ -> __ -> 'a1) -> 'a1 **)
176let rec memory_inj_rect_Type5 e1 m1 m2 h_mk_memory_inj =
177  h_mk_memory_inj __ __ __ __ __ __ __
178
179(** val memory_inj_rect_Type3 :
180    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
181    __ -> __ -> 'a1) -> 'a1 **)
182let rec memory_inj_rect_Type3 e1 m1 m2 h_mk_memory_inj =
183  h_mk_memory_inj __ __ __ __ __ __ __
184
185(** val memory_inj_rect_Type2 :
186    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
187    __ -> __ -> 'a1) -> 'a1 **)
188let rec memory_inj_rect_Type2 e1 m1 m2 h_mk_memory_inj =
189  h_mk_memory_inj __ __ __ __ __ __ __
190
191(** val memory_inj_rect_Type1 :
192    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
193    __ -> __ -> 'a1) -> 'a1 **)
194let rec memory_inj_rect_Type1 e1 m1 m2 h_mk_memory_inj =
195  h_mk_memory_inj __ __ __ __ __ __ __
196
197(** val memory_inj_rect_Type0 :
198    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
199    __ -> __ -> 'a1) -> 'a1 **)
200let rec memory_inj_rect_Type0 e1 m1 m2 h_mk_memory_inj =
201  h_mk_memory_inj __ __ __ __ __ __ __
202
203(** val memory_inj_inv_rect_Type4 :
204    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
205    __ -> __ -> __ -> 'a1) -> 'a1 **)
206let memory_inj_inv_rect_Type4 x1 x2 x3 h1 =
207  let hcut = memory_inj_rect_Type4 x1 x2 x3 h1 in hcut __
208
209(** val memory_inj_inv_rect_Type3 :
210    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
211    __ -> __ -> __ -> 'a1) -> 'a1 **)
212let memory_inj_inv_rect_Type3 x1 x2 x3 h1 =
213  let hcut = memory_inj_rect_Type3 x1 x2 x3 h1 in hcut __
214
215(** val memory_inj_inv_rect_Type2 :
216    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
217    __ -> __ -> __ -> 'a1) -> 'a1 **)
218let memory_inj_inv_rect_Type2 x1 x2 x3 h1 =
219  let hcut = memory_inj_rect_Type2 x1 x2 x3 h1 in hcut __
220
221(** val memory_inj_inv_rect_Type1 :
222    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
223    __ -> __ -> __ -> 'a1) -> 'a1 **)
224let memory_inj_inv_rect_Type1 x1 x2 x3 h1 =
225  let hcut = memory_inj_rect_Type1 x1 x2 x3 h1 in hcut __
226
227(** val memory_inj_inv_rect_Type0 :
228    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
229    __ -> __ -> __ -> 'a1) -> 'a1 **)
230let memory_inj_inv_rect_Type0 x1 x2 x3 h1 =
231  let hcut = memory_inj_rect_Type0 x1 x2 x3 h1 in hcut __
232
233(** val memory_inj_jmdiscr :
234    embedding -> GenMem.mem1 -> GenMem.mem1 -> __ **)
235let memory_inj_jmdiscr a1 a2 a3 =
236  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) __
237
238(** val typesize' : Csyntax.type0 -> Nat.nat **)
239let typesize' ty =
240  AST.typesize (Csyntax.typ_of_type ty)
241
Note: See TracBrowser for help on using the repository browser.