source: extracted/rTL.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: 3.4 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 rtl_seq =
122| Rtl_stack_address of Registers.register * Registers.register
123
124val rtl_seq_rect_Type4 :
125  (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1
126
127val rtl_seq_rect_Type5 :
128  (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1
129
130val rtl_seq_rect_Type3 :
131  (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1
132
133val rtl_seq_rect_Type2 :
134  (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1
135
136val rtl_seq_rect_Type1 :
137  (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1
138
139val rtl_seq_rect_Type0 :
140  (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1
141
142val rtl_seq_inv_rect_Type4 :
143  rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1
144
145val rtl_seq_inv_rect_Type3 :
146  rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1
147
148val rtl_seq_inv_rect_Type2 :
149  rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1
150
151val rtl_seq_inv_rect_Type1 :
152  rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1
153
154val rtl_seq_inv_rect_Type0 :
155  rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1
156
157val rtl_seq_discr : rtl_seq -> rtl_seq -> __
158
159val rtl_seq_jmdiscr : rtl_seq -> rtl_seq -> __
160
161val rTL_uns : Joint.unserialized_params
162
163val rTL_functs : Joint.get_pseudo_reg_functs
164
165val rTL : Joint.graph_params
166
167type rtl_program = Joint.joint_program
168
169val dpi1__o__reg_to_rtl_snd_argument__o__inject :
170  (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
171
172val eject__o__reg_to_rtl_snd_argument__o__inject :
173  Registers.register Types.sig0 -> Joint.psd_argument Types.sig0
174
175val reg_to_rtl_snd_argument__o__inject :
176  Registers.register -> Joint.psd_argument Types.sig0
177
178val dpi1__o__reg_to_rtl_snd_argument :
179  (Registers.register, 'a1) Types.dPair -> Joint.psd_argument
180
181val eject__o__reg_to_rtl_snd_argument :
182  Registers.register Types.sig0 -> Joint.psd_argument
183
184val dpi1__o__byte_to_rtl_snd_argument__o__inject :
185  (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
186
187val eject__o__byte_to_rtl_snd_argument__o__inject :
188  BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0
189
190val byte_to_rtl_snd_argument__o__inject :
191  BitVector.byte -> Joint.psd_argument Types.sig0
192
193val dpi1__o__byte_to_rtl_snd_argument :
194  (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument
195
196val eject__o__byte_to_rtl_snd_argument :
197  BitVector.byte Types.sig0 -> Joint.psd_argument
198
199val rTL_premain : rtl_program -> Joint.joint_closed_internal_function
200
Note: See TracBrowser for help on using the repository browser.