source: extracted/liveness.mli @ 2890

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

Exported again, now the execution is correct up to LIN for a simple program.

File size: 2.3 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 String
30
31open Sets
32
33open Listb
34
35open LabelledObjects
36
37open BitVectorTrie
38
39open Graphs
40
41open I8051
42
43open Order
44
45open Registers
46
47open CostLabel
48
49open Hide
50
51open Proper
52
53open PositiveMap
54
55open Deqsets
56
57open ErrorMessages
58
59open PreIdentifiers
60
61open Errors
62
63open Extralib
64
65open Lists
66
67open Identifiers
68
69open Integers
70
71open AST
72
73open Division
74
75open Exp
76
77open Arithmetic
78
79open Setoids
80
81open Monad
82
83open Option
84
85open Extranat
86
87open Vector
88
89open FoldStuff
90
91open BitVector
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107open ERTL
108
109open ERTLptr
110
111open Set_adt
112
113open Fixpoints
114
115val register_lattice : Fixpoints.property_lattice
116
117val rl_bottom : __
118
119val rl_psingleton : Registers.register -> __
120
121val rl_hsingleton : I8051.register -> __
122
123val pairwise :
124  ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a2 -> 'a2) -> ('a1, 'a2) Types.prod ->
125  ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod
126
127val rl_join : __ -> __ -> __
128
129val rl_diff : __ -> __ -> __
130
131val defined : AST.ident List.list -> Joint.joint_statement -> __
132
133val ret_regs : I8051.register Set_adt.set
134
135val rl_arg : Joint.psd_argument -> __
136
137val used :
138  AST.ident List.list -> Joint.joint_statement -> (Registers.register
139  Set_adt.set, I8051.register Set_adt.set) Types.prod
140
141val eliminable_step :
142  AST.ident List.list -> __ -> Joint.joint_step -> Bool.bool
143
144val eliminable :
145  AST.ident List.list -> __ -> Joint.joint_statement -> Bool.bool
146
147val statement_semantics :
148  AST.ident List.list -> Joint.joint_statement -> __ -> __
149
150val livebefore :
151  AST.ident List.list -> Joint.joint_internal_function ->
152  PreIdentifiers.identifier -> Fixpoints.valuation -> __
153
154val liveafter :
155  AST.ident List.list -> Joint.joint_internal_function ->
156  PreIdentifiers.identifier -> Fixpoints.valuation -> __
157
158val analyse_liveness :
159  Fixpoints.fixpoint_computer -> AST.ident List.list ->
160  Joint.joint_internal_function -> Fixpoints.valuation
161
162type vertex = (Registers.register, I8051.register) Types.sum
163
164val plives : Registers.register -> __ -> Bool.bool
165
166val hlives : I8051.register -> __ -> Bool.bool
167
168val lives : vertex -> __ -> Bool.bool
169
Note: See TracBrowser for help on using the repository browser.