source: extracted/values.mli @ 2649

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

...

File size: 3.3 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Coqlib
30
31open ErrorMessages
32
33open Option
34
35open Setoids
36
37open Monad
38
39open Positive
40
41open PreIdentifiers
42
43open Errors
44
45open Proper
46
47open PositiveMap
48
49open Deqsets
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Arithmetic
64
65open Extranat
66
67open Vector
68
69open FoldStuff
70
71open BitVector
72
73open Z
74
75open BitVectorZ
76
77open Pointers
78
79type val0 =
80| Vundef
81| Vint of AST.intsize * AST.bvint
82| Vnull
83| Vptr of Pointers.pointer
84
85val val_rect_Type4 :
86  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
87  'a1) -> val0 -> 'a1
88
89val val_rect_Type5 :
90  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
91  'a1) -> val0 -> 'a1
92
93val val_rect_Type3 :
94  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
95  'a1) -> val0 -> 'a1
96
97val val_rect_Type2 :
98  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
99  'a1) -> val0 -> 'a1
100
101val val_rect_Type1 :
102  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
103  'a1) -> val0 -> 'a1
104
105val val_rect_Type0 :
106  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
107  'a1) -> val0 -> 'a1
108
109val val_inv_rect_Type4 :
110  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
111  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
112
113val val_inv_rect_Type3 :
114  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
115  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
116
117val val_inv_rect_Type2 :
118  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
119  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
120
121val val_inv_rect_Type1 :
122  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
123  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
124
125val val_inv_rect_Type0 :
126  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
127  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
128
129val val_discr : val0 -> val0 -> __
130
131val val_jmdiscr : val0 -> val0 -> __
132
133val vzero : AST.intsize -> val0
134
135val vone : AST.intsize -> val0
136
137val mone0 : AST.intsize -> BitVector.bitVector
138
139val vmone : AST.intsize -> val0
140
141val vtrue : val0
142
143val vfalse : val0
144
145val of_bool : Bool.bool -> val0
146
147val eval_bool_of_val : val0 -> Bool.bool Errors.res
148
149val neg0 : val0 -> val0
150
151val notint : val0 -> val0
152
153val notbool0 : val0 -> val0
154
155val zero_ext1 : AST.intsize -> val0 -> val0
156
157val sign_ext1 : AST.intsize -> val0 -> val0
158
159val add0 : val0 -> val0 -> val0
160
161val sub : val0 -> val0 -> val0
162
163val mul0 : val0 -> val0 -> val0
164
165val v_and : val0 -> val0 -> val0
166
167val or1 : val0 -> val0 -> val0
168
169val xor0 : val0 -> val0 -> val0
170
171val cmp_match : Integers.comparison -> val0
172
173val cmp_mismatch : Integers.comparison -> val0
174
175val cmp_offset :
176  Integers.comparison -> Pointers.offset -> Pointers.offset -> Bool.bool
177
178val cmp_int :
179  Nat.nat -> Integers.comparison -> BitVector.bitVector ->
180  BitVector.bitVector -> Bool.bool
181
182val cmpu_int :
183  Nat.nat -> Integers.comparison -> BitVector.bitVector ->
184  BitVector.bitVector -> Bool.bool
185
186val cmp0 : Integers.comparison -> val0 -> val0 -> val0
187
188val cmpu0 : Integers.comparison -> val0 -> val0 -> val0
189
190val load_result : AST.typ -> val0 -> val0
191
Note: See TracBrowser for help on using the repository browser.