source: driver/extracted/rTLabs_abstract.mli @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 7.7 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open Graphs
6
7open Order
8
9open Registers
10
11open FrontEndOps
12
13open RTLabs_syntax
14
15open SmallstepExec
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.state
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_jmdiscr :
136  StructuredTraces.status_class -> StructuredTraces.status_class -> __
137
138type rTLabs_ext_state = { ras_state : RTLabs_semantics.state;
139                          ras_fn_stack : Pointers.block List.list }
140
141val rTLabs_ext_state_rect_Type4 :
142  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
143  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
144
145val rTLabs_ext_state_rect_Type5 :
146  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
147  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
148
149val rTLabs_ext_state_rect_Type3 :
150  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
151  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
152
153val rTLabs_ext_state_rect_Type2 :
154  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
155  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
156
157val rTLabs_ext_state_rect_Type1 :
158  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
159  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
160
161val rTLabs_ext_state_rect_Type0 :
162  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
163  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
164
165val ras_state :
166  RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state
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.state ->
173  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
174
175val rTLabs_ext_state_inv_rect_Type3 :
176  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
177  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
178
179val rTLabs_ext_state_inv_rect_Type2 :
180  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
181  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
182
183val rTLabs_ext_state_inv_rect_Type1 :
184  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
185  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
186
187val rTLabs_ext_state_inv_rect_Type0 :
188  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
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.state Types.sig0
200
201val eject__o__Ras_state__o__inject :
202  RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
203  RTLabs_semantics.state Types.sig0
204
205val ras_state__o__inject :
206  RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state
207  Types.sig0
208
209val dpi1__o__Ras_state :
210  RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
211  RTLabs_semantics.state
212
213val eject__o__Ras_state :
214  RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
215  RTLabs_semantics.state
216
217val next_state :
218  RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state ->
219  Events.trace -> rTLabs_ext_state
220
221val rTLabs_classify : RTLabs_semantics.state -> StructuredTraces.status_class
222
223val rTLabs_cost : RTLabs_semantics.state -> Bool.bool
224
225val rTLabs_cost_label :
226  RTLabs_semantics.state -> CostLabel.costlabel Types.option
227
228type rTLabs_pc =
229| Rapc_state of Pointers.block * Graphs.label
230| Rapc_call of Graphs.label Types.option * Pointers.block
231| Rapc_ret of Pointers.block Types.option
232| Rapc_fin
233
234val rTLabs_pc_rect_Type4 :
235  (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
236  Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
237  rTLabs_pc -> 'a1
238
239val rTLabs_pc_rect_Type5 :
240  (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
241  Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
242  rTLabs_pc -> 'a1
243
244val rTLabs_pc_rect_Type3 :
245  (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
246  Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
247  rTLabs_pc -> 'a1
248
249val rTLabs_pc_rect_Type2 :
250  (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
251  Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
252  rTLabs_pc -> 'a1
253
254val rTLabs_pc_rect_Type1 :
255  (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
256  Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
257  rTLabs_pc -> 'a1
258
259val rTLabs_pc_rect_Type0 :
260  (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
261  Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
262  rTLabs_pc -> 'a1
263
264val rTLabs_pc_inv_rect_Type4 :
265  rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
266  Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
267  Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
268
269val rTLabs_pc_inv_rect_Type3 :
270  rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
271  Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
272  Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
273
274val rTLabs_pc_inv_rect_Type2 :
275  rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
276  Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
277  Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
278
279val rTLabs_pc_inv_rect_Type1 :
280  rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
281  Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
282  Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
283
284val rTLabs_pc_inv_rect_Type0 :
285  rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
286  Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
287  Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
288
289val rTLabs_pc_discr : rTLabs_pc -> rTLabs_pc -> __
290
291val rTLabs_pc_jmdiscr : rTLabs_pc -> rTLabs_pc -> __
292
293val rTLabs_pc_eq : rTLabs_pc -> rTLabs_pc -> Bool.bool
294
295val rTLabs_deqset : Deqsets.deqSet
296
297val rTLabs_ext_state_to_pc : RTLabs_semantics.genv -> rTLabs_ext_state -> __
298
299val rTLabs_pc_to_cost_label :
300  RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t -> rTLabs_pc
301  -> CostLabel.costlabel Types.option
302
303val rTLabs_call_ident :
304  RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 -> AST.ident
305
306val rTLabs_status : RTLabs_semantics.genv -> StructuredTraces.abstract_status
307
308val eval_ext_statement :
309  RTLabs_semantics.genv -> rTLabs_ext_state -> (IO.io_out, IO.io_in,
310  (Events.trace, rTLabs_ext_state) Types.prod) IOMonad.iO
311
312val rTLabs_ext_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
313
314val make_ext_initial_state :
315  RTLabs_syntax.rTLabs_program -> rTLabs_ext_state Errors.res
316
317val rTLabs_ext_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
318
Note: See TracBrowser for help on using the repository browser.