source: extracted/liveness.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: 2.5 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Bool
10
11open Relations
12
13open Nat
14
15open Hints_declaration
16
17open Core_notation
18
19open Pts
20
21open Logic
22
23open Types
24
25open List
26
27open Util
28
29open Extra_bool
30
31open Coqlib
32
33open Values
34
35open FrontEndVal
36
37open GenMem
38
39open FrontEndMem
40
41open Globalenvs
42
43open String
44
45open Sets
46
47open Listb
48
49open LabelledObjects
50
51open BitVectorTrie
52
53open Graphs
54
55open I8051
56
57open Order
58
59open Registers
60
61open CostLabel
62
63open Hide
64
65open Proper
66
67open PositiveMap
68
69open Deqsets
70
71open ErrorMessages
72
73open PreIdentifiers
74
75open Errors
76
77open Extralib
78
79open Lists
80
81open Identifiers
82
83open Integers
84
85open AST
86
87open Division
88
89open Exp
90
91open Arithmetic
92
93open Setoids
94
95open Monad
96
97open Option
98
99open Extranat
100
101open Vector
102
103open FoldStuff
104
105open BitVector
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
123open ERTLptr
124
125open Set_adt
126
127open Fixpoints
128
129val rl_included :
130  (PreIdentifiers.identifier Set_adt.set, I8051.register Set_adt.set)
131  Types.prod -> (PreIdentifiers.identifier Set_adt.set, I8051.register
132  Set_adt.set) Types.prod -> Bool.bool
133
134val register_lattice : Fixpoints.property_lattice
135
136val rl_bottom : __
137
138val rl_psingleton : Registers.register -> __
139
140val rl_hsingleton : I8051.register -> __
141
142val pairwise :
143  ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a2 -> 'a2) -> ('a1, 'a2) Types.prod ->
144  ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod
145
146val rl_join : __ -> __ -> __
147
148val rl_diff : __ -> __ -> __
149
150val defined : AST.ident List.list -> Joint.joint_statement -> __
151
152val ret_regs : I8051.register Set_adt.set
153
154val rl_arg : Joint.psd_argument -> __
155
156val used :
157  AST.ident List.list -> Joint.joint_statement -> (Registers.register
158  Set_adt.set, I8051.register Set_adt.set) Types.prod
159
160val eliminable_step :
161  AST.ident List.list -> __ -> Joint.joint_step -> Bool.bool
162
163val eliminable :
164  AST.ident List.list -> __ -> Joint.joint_statement -> Bool.bool
165
166val statement_semantics :
167  AST.ident List.list -> Joint.joint_statement -> __ -> __
168
169val livebefore :
170  AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation
171  -> Fixpoints.valuation
172
173val liveafter :
174  AST.ident List.list -> Joint.joint_internal_function ->
175  PreIdentifiers.identifier -> Fixpoints.valuation -> __
176
177val analyse_liveness :
178  Fixpoints.fixpoint_computer -> AST.ident List.list ->
179  Joint.joint_internal_function -> Fixpoints.fixpoint
180
181type vertex = (Registers.register, I8051.register) Types.sum
182
183val plives : Registers.register -> __ -> Bool.bool
184
185val hlives : I8051.register -> __ -> Bool.bool
186
187val lives : vertex -> __ -> Bool.bool
188
Note: See TracBrowser for help on using the repository browser.