source: extracted/traces.mli @ 2829

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

Semantics files committed.

File size: 7.6 KB
Line 
1open Preamble
2
3open ExtraGlobalenvs
4
5open I8051bis
6
7open String
8
9open Sets
10
11open Listb
12
13open LabelledObjects
14
15open BitVectorTrie
16
17open Graphs
18
19open I8051
20
21open Order
22
23open Registers
24
25open BackEndOps
26
27open Joint
28
29open BEMem
30
31open CostLabel
32
33open Events
34
35open IOMonad
36
37open IO
38
39open Extra_bool
40
41open Coqlib
42
43open Values
44
45open FrontEndVal
46
47open Hide
48
49open ByteValues
50
51open Division
52
53open Z
54
55open BitVectorZ
56
57open Pointers
58
59open GenMem
60
61open FrontEndMem
62
63open Proper
64
65open PositiveMap
66
67open Deqsets
68
69open Extralib
70
71open Lists
72
73open Identifiers
74
75open Exp
76
77open Arithmetic
78
79open Vector
80
81open Div_and_mod
82
83open Util
84
85open FoldStuff
86
87open BitVector
88
89open Extranat
90
91open Integers
92
93open AST
94
95open ErrorMessages
96
97open Option
98
99open Setoids
100
101open Monad
102
103open Jmeq
104
105open Russell
106
107open Positive
108
109open PreIdentifiers
110
111open Bool
112
113open Relations
114
115open Nat
116
117open List
118
119open Hints_declaration
120
121open Core_notation
122
123open Pts
124
125open Logic
126
127open Types
128
129open Errors
130
131open Globalenvs
132
133open Joint_semantics
134
135open StructuredTraces
136
137type evaluation_params = { globals : AST.ident List.list;
138                           sparams : Joint_semantics.sem_params;
139                           ev_genv : Joint_semantics.genv }
140
141val evaluation_params_rect_Type4 :
142  (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
143  -> 'a1) -> evaluation_params -> 'a1
144
145val evaluation_params_rect_Type5 :
146  (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
147  -> 'a1) -> evaluation_params -> 'a1
148
149val evaluation_params_rect_Type3 :
150  (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
151  -> 'a1) -> evaluation_params -> 'a1
152
153val evaluation_params_rect_Type2 :
154  (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
155  -> 'a1) -> evaluation_params -> 'a1
156
157val evaluation_params_rect_Type1 :
158  (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
159  -> 'a1) -> evaluation_params -> 'a1
160
161val evaluation_params_rect_Type0 :
162  (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
163  -> 'a1) -> evaluation_params -> 'a1
164
165val globals : evaluation_params -> AST.ident List.list
166
167val sparams : evaluation_params -> Joint_semantics.sem_params
168
169val ev_genv : evaluation_params -> Joint_semantics.genv
170
171val evaluation_params_inv_rect_Type4 :
172  evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
173  Joint_semantics.genv -> __ -> 'a1) -> 'a1
174
175val evaluation_params_inv_rect_Type3 :
176  evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
177  Joint_semantics.genv -> __ -> 'a1) -> 'a1
178
179val evaluation_params_inv_rect_Type2 :
180  evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
181  Joint_semantics.genv -> __ -> 'a1) -> 'a1
182
183val evaluation_params_inv_rect_Type1 :
184  evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
185  Joint_semantics.genv -> __ -> 'a1) -> 'a1
186
187val evaluation_params_inv_rect_Type0 :
188  evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
189  Joint_semantics.genv -> __ -> 'a1) -> 'a1
190
191val evaluation_params_jmdiscr : evaluation_params -> evaluation_params -> __
192
193val sparams__o__msu_pars :
194  evaluation_params -> Joint.joint_closed_internal_function
195  Joint_semantics.sem_unserialized_params
196
197val sparams__o__msu_pars__o__st_pars :
198  evaluation_params -> Joint_semantics.sem_state_params
199
200val sparams__o__spp : evaluation_params -> Joint.params
201
202val sparams__o__spp__o__stmt_pars : evaluation_params -> Joint.stmt_params
203
204val sparams__o__spp__o__stmt_pars__o__uns_pars :
205  evaluation_params -> Joint.uns_params
206
207val sparams__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
208  evaluation_params -> Joint.unserialized_params
209
210type prog_params = { prog_spars : Joint_semantics.sem_params;
211                     prog : Joint.joint_program;
212                     stack_sizes : (AST.ident -> Nat.nat Types.option) }
213
214val prog_params_rect_Type4 :
215  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
216  Types.option) -> 'a1) -> prog_params -> 'a1
217
218val prog_params_rect_Type5 :
219  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
220  Types.option) -> 'a1) -> prog_params -> 'a1
221
222val prog_params_rect_Type3 :
223  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
224  Types.option) -> 'a1) -> prog_params -> 'a1
225
226val prog_params_rect_Type2 :
227  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
228  Types.option) -> 'a1) -> prog_params -> 'a1
229
230val prog_params_rect_Type1 :
231  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
232  Types.option) -> 'a1) -> prog_params -> 'a1
233
234val prog_params_rect_Type0 :
235  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
236  Types.option) -> 'a1) -> prog_params -> 'a1
237
238val prog_spars : prog_params -> Joint_semantics.sem_params
239
240val prog : prog_params -> Joint.joint_program
241
242val stack_sizes : prog_params -> AST.ident -> Nat.nat Types.option
243
244val prog_params_inv_rect_Type4 :
245  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
246  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
247
248val prog_params_inv_rect_Type3 :
249  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
250  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
251
252val prog_params_inv_rect_Type2 :
253  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
254  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
255
256val prog_params_inv_rect_Type1 :
257  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
258  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
259
260val prog_params_inv_rect_Type0 :
261  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
262  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
263
264val prog_params_jmdiscr : prog_params -> prog_params -> __
265
266val make_global : prog_params -> evaluation_params
267
268val prog_params_to_ev_params__o__sparams :
269  prog_params -> Joint_semantics.sem_params
270
271val prog_params_to_ev_params__o__sparams__o__msu_pars :
272  prog_params -> Joint.joint_closed_internal_function
273  Joint_semantics.sem_unserialized_params
274
275val prog_params_to_ev_params__o__sparams__o__msu_pars__o__st_pars :
276  prog_params -> Joint_semantics.sem_state_params
277
278val prog_params_to_ev_params__o__sparams__o__spp :
279  prog_params -> Joint.params
280
281val prog_params_to_ev_params__o__sparams__o__spp__o__stmt_pars :
282  prog_params -> Joint.stmt_params
283
284val prog_params_to_ev_params__o__sparams__o__spp__o__stmt_pars__o__uns_pars :
285  prog_params -> Joint.uns_params
286
287val prog_params_to_ev_params__o__sparams__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
288  prog_params -> Joint.unserialized_params
289
290val make_initial_state : prog_params -> Joint_semantics.state_pc Errors.res
291
292val joint_classify_step :
293  evaluation_params -> Joint.joint_step -> StructuredTraces.status_class
294
295val joint_classify_final :
296  evaluation_params -> Joint.joint_fin_step -> StructuredTraces.status_class
297
298val joint_classify :
299  evaluation_params -> Joint_semantics.state_pc ->
300  StructuredTraces.status_class
301
302val joint_call_ident :
303  evaluation_params -> Joint_semantics.state_pc -> AST.ident
304
305val joint_tailcall_ident :
306  evaluation_params -> Joint_semantics.state_pc -> AST.ident
307
308val pcDeq : Deqsets.deqSet
309
310val cost_label_of_stmt :
311  evaluation_params -> Joint.joint_statement -> CostLabel.costlabel
312  Types.option
313
314val joint_label_of_pc :
315  evaluation_params -> ByteValues.program_counter -> CostLabel.costlabel
316  Types.option
317
318val joint_abstract_status : prog_params -> StructuredTraces.abstract_status
319
320val joint_status :
321  Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
322  Types.option) -> StructuredTraces.abstract_status
323
Note: See TracBrowser for help on using the repository browser.