source: driver/extracted/joint_LTL_LIN.mli @ 3106

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

New extraction after ERTLptr abortion.

File size: 5.6 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
25open BitVectorTrie
26
27open Graphs
28
29open I8051
30
31open Order
32
33open Registers
34
35open CostLabel
36
37open Hide
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open Div_and_mod
78
79open Jmeq
80
81open Russell
82
83open List
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Types
92
93open Bool
94
95open Relations
96
97open Nat
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Positive
108
109open Z
110
111open BitVectorZ
112
113open Pointers
114
115open ByteValues
116
117open BackEndOps
118
119open Joint
120
121type registers_move =
122| From_acc of I8051.register * Types.unit0
123| To_acc of Types.unit0 * I8051.register
124| Int_to_reg of I8051.register * BitVector.byte
125| Int_to_acc of Types.unit0 * BitVector.byte
126
127val registers_move_rect_Type4 :
128  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
129  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
130  BitVector.byte -> 'a1) -> registers_move -> 'a1
131
132val registers_move_rect_Type5 :
133  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
134  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
135  BitVector.byte -> 'a1) -> registers_move -> 'a1
136
137val registers_move_rect_Type3 :
138  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
139  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
140  BitVector.byte -> 'a1) -> registers_move -> 'a1
141
142val registers_move_rect_Type2 :
143  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
144  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
145  BitVector.byte -> 'a1) -> registers_move -> 'a1
146
147val registers_move_rect_Type1 :
148  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
149  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
150  BitVector.byte -> 'a1) -> registers_move -> 'a1
151
152val registers_move_rect_Type0 :
153  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
154  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
155  BitVector.byte -> 'a1) -> registers_move -> 'a1
156
157val registers_move_inv_rect_Type4 :
158  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
159  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
160  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
161  'a1) -> 'a1
162
163val registers_move_inv_rect_Type3 :
164  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
165  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
166  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
167  'a1) -> 'a1
168
169val registers_move_inv_rect_Type2 :
170  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
171  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
172  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
173  'a1) -> 'a1
174
175val registers_move_inv_rect_Type1 :
176  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
177  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
178  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
179  'a1) -> 'a1
180
181val registers_move_inv_rect_Type0 :
182  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
183  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
184  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
185  'a1) -> 'a1
186
187val registers_move_discr : registers_move -> registers_move -> __
188
189val registers_move_jmdiscr : registers_move -> registers_move -> __
190
191type ltl_lin_seq =
192| SAVE_CARRY
193| RESTORE_CARRY
194| LOW_ADDRESS of Graphs.label
195| HIGH_ADDRESS of Graphs.label
196
197val ltl_lin_seq_rect_Type4 :
198  'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
199  -> 'a1
200
201val ltl_lin_seq_rect_Type5 :
202  'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
203  -> 'a1
204
205val ltl_lin_seq_rect_Type3 :
206  'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
207  -> 'a1
208
209val ltl_lin_seq_rect_Type2 :
210  'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
211  -> 'a1
212
213val ltl_lin_seq_rect_Type1 :
214  'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
215  -> 'a1
216
217val ltl_lin_seq_rect_Type0 :
218  'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
219  -> 'a1
220
221val ltl_lin_seq_inv_rect_Type4 :
222  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
223  (Graphs.label -> __ -> 'a1) -> 'a1
224
225val ltl_lin_seq_inv_rect_Type3 :
226  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
227  (Graphs.label -> __ -> 'a1) -> 'a1
228
229val ltl_lin_seq_inv_rect_Type2 :
230  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
231  (Graphs.label -> __ -> 'a1) -> 'a1
232
233val ltl_lin_seq_inv_rect_Type1 :
234  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
235  (Graphs.label -> __ -> 'a1) -> 'a1
236
237val ltl_lin_seq_inv_rect_Type0 :
238  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
239  (Graphs.label -> __ -> 'a1) -> 'a1
240
241val ltl_lin_seq_discr : ltl_lin_seq -> ltl_lin_seq -> __
242
243val ltl_lin_seq_jmdiscr : ltl_lin_seq -> ltl_lin_seq -> __
244
245val ltl_lin_seq_labels : ltl_lin_seq -> Graphs.label List.list
246
247val lTL_LIN_uns : Joint.unserialized_params
248
249val lTL_LIN_functs : Joint.get_pseudo_reg_functs
250
251val lTL_LIN : Joint.uns_params
252
Note: See TracBrowser for help on using the repository browser.