source: extracted/eRTLptr.mli @ 2890

Last change on this file since 2890 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: 4.5 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
107open ERTL
108
109type ertlptr_seq =
110| Ertlptr_ertl of ERTL.ertl_seq
111| LOW_ADDRESS of Registers.register * Graphs.label
112| HIGH_ADDRESS of Registers.register * Graphs.label
113
114val ertlptr_seq_rect_Type4 :
115  (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
116  (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1
117
118val ertlptr_seq_rect_Type5 :
119  (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
120  (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1
121
122val ertlptr_seq_rect_Type3 :
123  (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
124  (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1
125
126val ertlptr_seq_rect_Type2 :
127  (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
128  (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1
129
130val ertlptr_seq_rect_Type1 :
131  (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
132  (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1
133
134val ertlptr_seq_rect_Type0 :
135  (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
136  (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1
137
138val ertlptr_seq_inv_rect_Type4 :
139  ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
140  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __ ->
141  'a1) -> 'a1
142
143val ertlptr_seq_inv_rect_Type3 :
144  ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
145  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __ ->
146  'a1) -> 'a1
147
148val ertlptr_seq_inv_rect_Type2 :
149  ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
150  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __ ->
151  'a1) -> 'a1
152
153val ertlptr_seq_inv_rect_Type1 :
154  ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
155  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __ ->
156  'a1) -> 'a1
157
158val ertlptr_seq_inv_rect_Type0 :
159  ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
160  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __ ->
161  'a1) -> 'a1
162
163val ertlptr_seq_discr : ertlptr_seq -> ertlptr_seq -> __
164
165val ertlptr_seq_jmdiscr : ertlptr_seq -> ertlptr_seq -> __
166
167val eRTLptr_uns : Joint.unserialized_params
168
169val eRTLptr_functs : Joint.get_pseudo_reg_functs
170
171val eRTLptr : Joint.graph_params
172
173type ertlptr_program = Joint.joint_program
174
175val ertlptr_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq
176
177val dpi1__o__ertlptr_seq_to_joint_seq__o__inject :
178  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq Types.sig0
179
180val dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
181  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step Types.sig0
182
183val dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step :
184  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
185
186val eject__o__ertlptr_seq_to_joint_seq__o__inject :
187  AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0
188
189val eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
190  AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0
191
192val eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step :
193  AST.ident List.list -> __ Types.sig0 -> Joint.joint_step
194
195val ertlptr_seq_to_joint_seq__o__seq_to_step :
196  AST.ident List.list -> __ -> Joint.joint_step
197
198val ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
199  AST.ident List.list -> __ -> Joint.joint_step Types.sig0
200
201val ertlptr_seq_to_joint_seq__o__inject :
202  AST.ident List.list -> __ -> Joint.joint_seq Types.sig0
203
204val dpi1__o__ertlptr_seq_to_joint_seq :
205  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
206
207val eject__o__ertlptr_seq_to_joint_seq :
208  AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq
209
Note: See TracBrowser for help on using the repository browser.