source: driver/extracted/liveness.mli @ 3106

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

New extraction after ERTLptr abortion.

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 Set_adt
124
125open Fixpoints
126
127val 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
132val register_lattice : Fixpoints.property_lattice
133
134val rl_bottom : __
135
136val rl_psingleton : Registers.register -> __
137
138val rl_hsingleton : I8051.register -> __
139
140val pairwise :
141  ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a2 -> 'a2) -> ('a1, 'a2) Types.prod ->
142  ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod
143
144val rl_join : __ -> __ -> __
145
146val rl_diff : __ -> __ -> __
147
148val defined : AST.ident List.list -> Joint.joint_statement -> __
149
150val ret_regs : I8051.register Set_adt.set
151
152val rl_arg : Joint.psd_argument -> __
153
154val used :
155  AST.ident List.list -> Joint.joint_statement -> (Registers.register
156  Set_adt.set, I8051.register Set_adt.set) Types.prod
157
158val eliminable_step :
159  AST.ident List.list -> __ -> Joint.joint_step -> Bool.bool
160
161val eliminable :
162  AST.ident List.list -> __ -> Joint.joint_statement -> Bool.bool
163
164val statement_semantics :
165  AST.ident List.list -> Joint.joint_statement -> __ -> __
166
167val livebefore :
168  AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation
169  -> Fixpoints.valuation
170
171val liveafter :
172  AST.ident List.list -> Joint.joint_internal_function ->
173  PreIdentifiers.identifier -> Fixpoints.valuation -> __
174
175val analyse_liveness :
176  Fixpoints.fixpoint_computer -> AST.ident List.list ->
177  Joint.joint_internal_function -> Fixpoints.fixpoint
178
179type vertex = (Registers.register, I8051.register) Types.sum
180
181val plives : Registers.register -> __ -> Bool.bool
182
183val hlives : I8051.register -> __ -> Bool.bool
184
185val lives : vertex -> __ -> Bool.bool
186
Note: See TracBrowser for help on using the repository browser.