extracted/rTL.mli

   1 open Preamble
   2
   3 open Extra_bool
   4
   5 open Coqlib
   6
   7 open Values
   8
   9 open FrontEndVal
  10
  11 open GenMem
  12
  13 open FrontEndMem
  14
  15 open Globalenvs
  16
  17 open String
  18
  19 open Sets
  20
  21 open Listb
  22
  23 open LabelledObjects
  24
  25 open BitVectorTrie
  26
  27 open Graphs
  28
  29 open I8051
  30
  31 open Order
  32
  33 open Registers
  34
  35 open CostLabel
  36
  37 open Hide
  38
  39 open Proper
  40
  41 open PositiveMap
  42
  43 open Deqsets
  44
  45 open ErrorMessages
  46
  47 open PreIdentifiers
  48
  49 open Errors
  50
  51 open Extralib
  52
  53 open Lists
  54
  55 open Identifiers
  56
  57 open Integers
  58
  59 open AST
  60
  61 open Division
  62
  63 open Exp
  64
  65 open Arithmetic
  66
  67 open Setoids
  68
  69 open Monad
  70
  71 open Option
  72
  73 open Extranat
  74
  75 open Vector
  76
  77 open Div_and_mod
  78
  79 open Jmeq
  80
  81 open Russell
  82
  83 open List
  84
  85 open Util
  86
  87 open FoldStuff
  88
  89 open BitVector
  90
  91 open Types
  92
  93 open Bool
  94
  95 open Relations
  96
  97 open Nat
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 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 type rtl_seq =
 122 | Rtl_stack_address of Registers.register * Registers.register
 123
 124 val rtl_seq_rect_Type4 :
 125   (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1
 126
 127 val rtl_seq_rect_Type5 :
 128   (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1
 129
 130 val rtl_seq_rect_Type3 :
 131   (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1
 132
 133 val rtl_seq_rect_Type2 :
 134   (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1
 135
 136 val rtl_seq_rect_Type1 :
 137   (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1
 138
 139 val rtl_seq_rect_Type0 :
 140   (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1
 141
 142 val rtl_seq_inv_rect_Type4 :
 143   rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1
 144
 145 val rtl_seq_inv_rect_Type3 :
 146   rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1
 147
 148 val rtl_seq_inv_rect_Type2 :
 149   rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1
 150
 151 val rtl_seq_inv_rect_Type1 :
 152   rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1
 153
 154 val rtl_seq_inv_rect_Type0 :
 155   rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1
 156
 157 val rtl_seq_discr : rtl_seq -> rtl_seq -> __
 158
 159 val rtl_seq_jmdiscr : rtl_seq -> rtl_seq -> __
 160
 161 val rTL_uns : Joint.unserialized_params
 162
 163 val rTL_functs : Joint.get_pseudo_reg_functs
 164
 165 val rTL : Joint.graph_params
 166
 167 type rtl_program = Joint.joint_program
 168
 169 val dpi1__o__reg_to_rtl_snd_argument__o__inject :
 170   (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
 171
 172 val eject__o__reg_to_rtl_snd_argument__o__inject :
 173   Registers.register Types.sig0 -> Joint.psd_argument Types.sig0
 174
 175 val reg_to_rtl_snd_argument__o__inject :
 176   Registers.register -> Joint.psd_argument Types.sig0
 177
 178 val dpi1__o__reg_to_rtl_snd_argument :
 179   (Registers.register, 'a1) Types.dPair -> Joint.psd_argument
 180
 181 val eject__o__reg_to_rtl_snd_argument :
 182   Registers.register Types.sig0 -> Joint.psd_argument
 183
 184 val dpi1__o__byte_to_rtl_snd_argument__o__inject :
 185   (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
 186
 187 val eject__o__byte_to_rtl_snd_argument__o__inject :
 188   BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0
 189
 190 val byte_to_rtl_snd_argument__o__inject :
 191   BitVector.byte -> Joint.psd_argument Types.sig0
 192
 193 val dpi1__o__byte_to_rtl_snd_argument :
 194   (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument
 195
 196 val eject__o__byte_to_rtl_snd_argument :
 197   BitVector.byte Types.sig0 -> Joint.psd_argument
 198
 199 val rTL_premain : rtl_program -> Joint.joint_closed_internal_function
 200