source: extracted/rTLabs_abstract.mli @ 2746

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

Exported again.
File size: 7.3 KB
Line 
1open Preamble
2
3open Graphs
4
5open Order
6
7open Registers
8
9open FrontEndOps
10
11open RTLabs_syntax
12
13open SmallstepExec
14
15open BitVectorTrie
16
17open CostLabel
18
19open Events
20
21open IOMonad
22
23open IO
24
25open Extra_bool
26
27open Coqlib
28
29open Values
30
31open FrontEndVal
32
33open Hide
34
35open ByteValues
36
37open Division
38
39open Z
40
41open BitVectorZ
42
43open Pointers
44
45open GenMem
46
47open FrontEndMem
48
49open Proper
50
51open PositiveMap
52
53open Deqsets
54
55open Extralib
56
57open Lists
58
59open Identifiers
60
61open Exp
62
63open Arithmetic
64
65open Vector
66
67open Div_and_mod
68
69open Util
70
71open FoldStuff
72
73open BitVector
74
75open Extranat
76
77open Integers
78
79open AST
80
81open Globalenvs
82
83open ErrorMessages
84
85open Option
86
87open Setoids
88
89open Monad
90
91open Jmeq
92
93open Russell
94
95open Positive
96
97open PreIdentifiers
98
99open Errors
100
101open Bool
102
103open Relations
104
105open Nat
106
107open Hints_declaration
108
109open Core_notation
110
111open Pts
112
113open Logic
114
115open Types
116
117open List
118
119open RTLabs_semantics
120
121type rTLabs_state = RTLabs_semantics.state0
122
123type rTLabs_genv = RTLabs_semantics.genv
124
125open Sets
126
127open Listb
128
129open StructuredTraces
130
131open CostSpec
132
133open Deqsets_extra
134
135val status_class_jmdiscr0 :
136  StructuredTraces.status_class -> StructuredTraces.status_class -> __
137
138type rTLabs_ext_state = { ras_state : RTLabs_semantics.state0;
139                          ras_fn_stack : Pointers.block List.list }
140
141val rTLabs_ext_state_rect_Type4 :
142  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
143  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
144
145val rTLabs_ext_state_rect_Type5 :
146  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
147  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
148
149val rTLabs_ext_state_rect_Type3 :
150  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
151  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
152
153val rTLabs_ext_state_rect_Type2 :
154  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
155  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
156
157val rTLabs_ext_state_rect_Type1 :
158  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
159  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
160
161val rTLabs_ext_state_rect_Type0 :
162  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
163  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
164
165val ras_state :
166  RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state0
167
168val ras_fn_stack :
169  RTLabs_semantics.genv -> rTLabs_ext_state -> Pointers.block List.list
170
171val rTLabs_ext_state_inv_rect_Type4 :
172  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state0 ->
173  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
174
175val rTLabs_ext_state_inv_rect_Type3 :
176  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state0 ->
177  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
178
179val rTLabs_ext_state_inv_rect_Type2 :
180  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state0 ->
181  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
182
183val rTLabs_ext_state_inv_rect_Type1 :
184  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state0 ->
185  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
186
187val rTLabs_ext_state_inv_rect_Type0 :
188  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state0 ->
189  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
190
191val rTLabs_ext_state_discr :
192  RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __
193
194val rTLabs_ext_state_jmdiscr :
195  RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __
196
197val dpi1__o__Ras_state__o__inject :
198  RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
199  RTLabs_semantics.state0 Types.sig0
200
201val eject__o__Ras_state__o__inject :
202  RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
203  RTLabs_semantics.state0 Types.sig0
204
205val ras_state__o__inject :
206  RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state0
207  Types.sig0
208
209val dpi1__o__Ras_state :
210  RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
211  RTLabs_semantics.state0
212
213val eject__o__Ras_state :
214  RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
215  RTLabs_semantics.state0
216
217val next_state :
218  RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state0 ->
219  Events.trace -> rTLabs_ext_state
220
221val rTLabs_classify :
222  RTLabs_semantics.state0 -> StructuredTraces.status_class
223
224val rTLabs_cost : RTLabs_semantics.state0 -> Bool.bool
225
226val rTLabs_cost_label :
227  RTLabs_semantics.state0 -> CostLabel.costlabel Types.option
228
229type rTLabs_pc =
230| Rapc_state of Pointers.block * Graphs.label
231| Rapc_call of Graphs.label Types.option * Pointers.block
232| Rapc_ret of Pointers.block Types.option
233| Rapc_fin
234
235val rTLabs_pc_rect_Type4 :
236  (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
237  Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
238  rTLabs_pc -> 'a1
239
240val rTLabs_pc_rect_Type5 :
241  (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
242  Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
243  rTLabs_pc -> 'a1
244
245val rTLabs_pc_rect_Type3 :
246  (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
247  Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
248  rTLabs_pc -> 'a1
249
250val rTLabs_pc_rect_Type2 :
251  (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
252  Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
253  rTLabs_pc -> 'a1
254
255val rTLabs_pc_rect_Type1 :
256  (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
257  Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
258  rTLabs_pc -> 'a1
259
260val rTLabs_pc_rect_Type0 :
261  (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
262  Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
263  rTLabs_pc -> 'a1
264
265val rTLabs_pc_inv_rect_Type4 :
266  rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
267  Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
268  Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
269
270val rTLabs_pc_inv_rect_Type3 :
271  rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
272  Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
273  Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
274
275val rTLabs_pc_inv_rect_Type2 :
276  rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
277  Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
278  Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
279
280val rTLabs_pc_inv_rect_Type1 :
281  rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
282  Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
283  Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
284
285val rTLabs_pc_inv_rect_Type0 :
286  rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
287  Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
288  Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
289
290val rTLabs_pc_discr : rTLabs_pc -> rTLabs_pc -> __
291
292val rTLabs_pc_jmdiscr : rTLabs_pc -> rTLabs_pc -> __
293
294val rTLabs_pc_eq : rTLabs_pc -> rTLabs_pc -> Bool.bool
295
296val rTLabs_deqset : Deqsets.deqSet
297
298val rTLabs_ext_state_to_pc : RTLabs_semantics.genv -> rTLabs_ext_state -> __
299
300val rTLabs_pc_to_cost_label :
301  RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t -> rTLabs_pc
302  -> CostLabel.costlabel Types.option
303
304val rTLabs_call_ident :
305  RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 -> AST.ident
306
307val rTLabs_status : RTLabs_semantics.genv -> StructuredTraces.abstract_status
308
Note: See TracBrowser for help on using the repository browser.