source: extracted/eRTLptr.mli @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 4.7 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
121open ERTL
122
123type ertlptr_seq =
124| Ertlptr_ertl of ERTL.ertl_seq
125| LOW_ADDRESS of Registers.register * Graphs.label
126| HIGH_ADDRESS of Registers.register * Graphs.label
127
128val ertlptr_seq_rect_Type4 :
129  (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
130  (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1
131
132val ertlptr_seq_rect_Type5 :
133  (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
134  (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1
135
136val ertlptr_seq_rect_Type3 :
137  (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
138  (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1
139
140val ertlptr_seq_rect_Type2 :
141  (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
142  (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1
143
144val ertlptr_seq_rect_Type1 :
145  (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
146  (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1
147
148val ertlptr_seq_rect_Type0 :
149  (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
150  (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1
151
152val ertlptr_seq_inv_rect_Type4 :
153  ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
154  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __ ->
155  'a1) -> 'a1
156
157val ertlptr_seq_inv_rect_Type3 :
158  ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
159  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __ ->
160  'a1) -> 'a1
161
162val ertlptr_seq_inv_rect_Type2 :
163  ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
164  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __ ->
165  'a1) -> 'a1
166
167val ertlptr_seq_inv_rect_Type1 :
168  ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
169  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __ ->
170  'a1) -> 'a1
171
172val ertlptr_seq_inv_rect_Type0 :
173  ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
174  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __ ->
175  'a1) -> 'a1
176
177val ertlptr_seq_discr : ertlptr_seq -> ertlptr_seq -> __
178
179val ertlptr_seq_jmdiscr : ertlptr_seq -> ertlptr_seq -> __
180
181val eRTLptr_uns : Joint.unserialized_params
182
183val eRTLptr_functs : Joint.get_pseudo_reg_functs
184
185val eRTLptr : Joint.graph_params
186
187type ertlptr_program = Joint.joint_program
188
189val ertlptr_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq
190
191val dpi1__o__ertlptr_seq_to_joint_seq__o__inject :
192  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq Types.sig0
193
194val dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
195  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step Types.sig0
196
197val dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step :
198  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
199
200val eject__o__ertlptr_seq_to_joint_seq__o__inject :
201  AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0
202
203val eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
204  AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0
205
206val eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step :
207  AST.ident List.list -> __ Types.sig0 -> Joint.joint_step
208
209val ertlptr_seq_to_joint_seq__o__seq_to_step :
210  AST.ident List.list -> __ -> Joint.joint_step
211
212val ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
213  AST.ident List.list -> __ -> Joint.joint_step Types.sig0
214
215val ertlptr_seq_to_joint_seq__o__inject :
216  AST.ident List.list -> __ -> Joint.joint_seq Types.sig0
217
218val dpi1__o__ertlptr_seq_to_joint_seq :
219  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
220
221val eject__o__ertlptr_seq_to_joint_seq :
222  AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq
223
224val eRTLptr_premain : ertlptr_program -> Joint.joint_closed_internal_function
225
Note: See TracBrowser for help on using the repository browser.