source: extracted/compiler.mli @ 2649

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

...

File size: 2.3 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Setoids
22
23open Monad
24
25open Option
26
27open Lists
28
29open Positive
30
31open Identifiers
32
33open Arithmetic
34
35open Vector
36
37open Div_and_mod
38
39open Jmeq
40
41open Russell
42
43open List
44
45open Util
46
47open FoldStuff
48
49open BitVector
50
51open Extranat
52
53open Bool
54
55open Relations
56
57open Nat
58
59open Integers
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Types
70
71open AST
72
73open Csyntax
74
75open Label
76
77open Sets
78
79open Listb
80
81open Star
82
83open Frontend_misc
84
85open CexecInd
86
87open CexecSound
88
89open Casts
90
91open ClassifyOp
92
93open Smallstep
94
95open Extra_bool
96
97open FrontEndVal
98
99open Hide
100
101open ByteValues
102
103open GenMem
104
105open FrontEndMem
106
107open Globalenvs
108
109open Csem
110
111open SmallstepExec
112
113open Division
114
115open Z
116
117open BitVectorZ
118
119open Pointers
120
121open Values
122
123open Events
124
125open IOMonad
126
127open IO
128
129open Cexec
130
131open TypeComparison
132
133open SimplifyCasts
134
135open MemProperties
136
137open MemoryInjections
138
139open Fresh
140
141open SwitchRemoval
142
143open FrontEndOps
144
145open Cminor_syntax
146
147open ToCminor
148
149open Initialisation
150
151open BitVectorTrie
152
153open Graphs
154
155open Order
156
157open Registers
158
159open RTLabs_syntax
160
161open ToRTLabs
162
163val front_end :
164  Csyntax.clight_program -> ((CostLabel.costlabel, Csyntax.clight_program)
165  Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res
166
167open String
168
169open LabelledObjects
170
171open ASM
172
173val back_end : RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program
174
175type object_code = BitVector.byte List.list
176
177type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
178
179val assembler :
180  ASM.pseudo_assembly_program -> (object_code, costlabel_map) Types.prod
181  Errors.res
182
183open StructuredTraces
184
185open AbstractStatus
186
187open Status
188
189open StatusProofs
190
191open Interpret
192
193open Fetch
194
195open ASMCosts
196
197val lift_cost_map_back_to_front :
198  Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
199  CostLabel.costlabel BitVectorTrie.bitVectorTrie -> (CostLabel.costlabel ->
200  (__, __) Types.sum) -> StructuredTraces.as_cost_map ->
201  Label.clight_cost_map
202
203open UtilBranch
204
205open ASMCostsSplit
206
207val compile :
208  Csyntax.clight_program -> ((object_code, costlabel_map) Types.prod,
209  (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
210  Errors.res
211
Note: See TracBrowser for help on using the repository browser.