source: extracted/liveness.mli @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 8 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 2.0 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 rl_join : __ -> __ -> __
124
125val rl_diff : __ -> __ -> __
126
127val defined : AST.ident List.list -> Joint.joint_statement -> __
128
129val ret_regs : I8051.register Set_adt.set
130
131val rl_arg : Joint.psd_argument -> __
132
133val used :
134  AST.ident List.list -> Joint.joint_statement -> (Registers.register
135  Set_adt.set, I8051.register Set_adt.set) Types.prod
136
137val eliminable :
138  AST.ident List.list -> __ -> Joint.joint_statement -> __ Types.option
139
140val statement_semantics :
141  AST.ident List.list -> Joint.joint_statement -> __ -> __
142
143val livebefore :
144  AST.ident List.list -> Joint.joint_internal_function ->
145  PreIdentifiers.identifier -> Fixpoints.valuation -> __
146
147val liveafter :
148  AST.ident List.list -> Joint.joint_internal_function ->
149  PreIdentifiers.identifier -> Fixpoints.valuation -> __
150
151val analyse_liveness :
152  Fixpoints.fixpoint_computer -> AST.ident List.list ->
153  Joint.joint_internal_function -> Fixpoints.valuation
154
155type vertex = (Registers.register, I8051.register) Types.sum
156
157val plives : Registers.register -> __ -> Bool.bool
158
159val hlives : I8051.register -> __ -> Bool.bool
160
161val lives : vertex -> __ -> Bool.bool
162
Note: See TracBrowser for help on using the repository browser.