source: extracted/memoryInjections.mli @ 2649

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

...

File size: 2.9 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
127val zoo : Pointers.offset -> Z.z
128
129val boo : Z.z -> Pointers.offset
130
131val block_decidable_eq :
132  Pointers.block -> Pointers.block -> (__, __) Types.sum
133
134type embedding =
135  Pointers.block -> (Pointers.block, Pointers.offset) Types.prod Types.option
136
137val offset_plus : Pointers.offset -> Pointers.offset -> Pointers.offset
138
139val pointer_translation :
140  Pointers.pointer -> embedding -> Pointers.pointer Types.option
141
142val memory_inj_rect_Type4 :
143  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
144  __ -> __ -> 'a1) -> 'a1
145
146val memory_inj_rect_Type5 :
147  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
148  __ -> __ -> 'a1) -> 'a1
149
150val memory_inj_rect_Type3 :
151  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
152  __ -> __ -> 'a1) -> 'a1
153
154val memory_inj_rect_Type2 :
155  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
156  __ -> __ -> 'a1) -> 'a1
157
158val memory_inj_rect_Type1 :
159  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
160  __ -> __ -> 'a1) -> 'a1
161
162val memory_inj_rect_Type0 :
163  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
164  __ -> __ -> 'a1) -> 'a1
165
166val memory_inj_inv_rect_Type4 :
167  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
168  __ -> __ -> __ -> 'a1) -> 'a1
169
170val memory_inj_inv_rect_Type3 :
171  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
172  __ -> __ -> __ -> 'a1) -> 'a1
173
174val memory_inj_inv_rect_Type2 :
175  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
176  __ -> __ -> __ -> 'a1) -> 'a1
177
178val memory_inj_inv_rect_Type1 :
179  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
180  __ -> __ -> __ -> 'a1) -> 'a1
181
182val memory_inj_inv_rect_Type0 :
183  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
184  __ -> __ -> __ -> 'a1) -> 'a1
185
186val memory_inj_jmdiscr : embedding -> GenMem.mem1 -> GenMem.mem1 -> __
187
188val typesize' : Csyntax.type0 -> Nat.nat
189
Note: See TracBrowser for help on using the repository browser.