source: extracted/rTL.mli @ 2817

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

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

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