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