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
RevLine 
[2717]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
[2951]29open Extra_bool
30
31open Coqlib
32
33open Values
34
35open FrontEndVal
36
37open GenMem
38
39open FrontEndMem
40
41open Globalenvs
42
[2717]43open String
44
45open Sets
46
47open Listb
48
49open LabelledObjects
50
[2773]51open BitVectorTrie
52
[2717]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
[2773]93open Setoids
94
95open Monad
96
97open Option
98
[2717]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
[2951]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
[2730]134val register_lattice : Fixpoints.property_lattice
[2717]135
[2730]136val rl_bottom : __
[2717]137
138val rl_psingleton : Registers.register -> __
139
140val rl_hsingleton : I8051.register -> __
141
[2890]142val pairwise :
143  ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a2 -> 'a2) -> ('a1, 'a2) Types.prod ->
144  ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod
145
[2717]146val rl_join : __ -> __ -> __
147
148val rl_diff : __ -> __ -> __
149
150val defined : AST.ident List.list -> Joint.joint_statement -> __
151
[2730]152val ret_regs : I8051.register Set_adt.set
[2717]153
154val rl_arg : Joint.psd_argument -> __
155
156val used :
157  AST.ident List.list -> Joint.joint_statement -> (Registers.register
[2730]158  Set_adt.set, I8051.register Set_adt.set) Types.prod
[2717]159
[2890]160val eliminable_step :
161  AST.ident List.list -> __ -> Joint.joint_step -> Bool.bool
162
[2717]163val eliminable :
[2890]164  AST.ident List.list -> __ -> Joint.joint_statement -> Bool.bool
[2717]165
166val statement_semantics :
167  AST.ident List.list -> Joint.joint_statement -> __ -> __
168
169val livebefore :
[2951]170  AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation
171  -> Fixpoints.valuation
[2717]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 ->
[2951]179  Joint.joint_internal_function -> Fixpoints.fixpoint
[2717]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.