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