133 open Hints_declaration
151 open StructuredTraces
153 type evaluation_params = { globals : AST.ident List.list;
154 ev_genv : Joint_semantics.genv }
156 val evaluation_params_rect_Type4 :
157 Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
158 -> 'a1) -> evaluation_params -> 'a1
160 val evaluation_params_rect_Type5 :
161 Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
162 -> 'a1) -> evaluation_params -> 'a1
164 val evaluation_params_rect_Type3 :
165 Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
166 -> 'a1) -> evaluation_params -> 'a1
168 val evaluation_params_rect_Type2 :
169 Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
170 -> 'a1) -> evaluation_params -> 'a1
172 val evaluation_params_rect_Type1 :
173 Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
174 -> 'a1) -> evaluation_params -> 'a1
176 val evaluation_params_rect_Type0 :
177 Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
178 -> 'a1) -> evaluation_params -> 'a1
181 Joint_semantics.sem_params -> evaluation_params -> AST.ident List.list
184 Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
186 val evaluation_params_inv_rect_Type4 :
187 Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
188 Joint_semantics.genv -> __ -> 'a1) -> 'a1
190 val evaluation_params_inv_rect_Type3 :
191 Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
192 Joint_semantics.genv -> __ -> 'a1) -> 'a1
194 val evaluation_params_inv_rect_Type2 :
195 Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
196 Joint_semantics.genv -> __ -> 'a1) -> 'a1
198 val evaluation_params_inv_rect_Type1 :
199 Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
200 Joint_semantics.genv -> __ -> 'a1) -> 'a1
202 val evaluation_params_inv_rect_Type0 :
203 Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
204 Joint_semantics.genv -> __ -> 'a1) -> 'a1
206 val evaluation_params_discr :
207 Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> __
209 val evaluation_params_jmdiscr :
210 Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> __
212 val dpi1__o__ev_genv__o__inject :
213 Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
214 Joint_semantics.genv Types.sig0
216 val dpi1__o__ev_genv__o__ge__o__inject :
217 Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
218 Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
221 val dpi1__o__ev_genv__o__ge :
222 Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
223 Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
225 val eject__o__ev_genv__o__inject :
226 Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
227 Joint_semantics.genv Types.sig0
229 val eject__o__ev_genv__o__ge__o__inject :
230 Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
231 Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
234 val eject__o__ev_genv__o__ge :
235 Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
236 Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
239 Joint_semantics.sem_params -> evaluation_params ->
240 Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
242 val ev_genv__o__ge__o__inject :
243 Joint_semantics.sem_params -> evaluation_params ->
244 Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
247 val ev_genv__o__inject :
248 Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
251 val dpi1__o__ev_genv :
252 Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
255 val eject__o__ev_genv :
256 Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
259 type prog_params = { prog_spars : Joint_semantics.sem_params;
260 prog : Joint.joint_program;
261 stack_sizes : (AST.ident -> Nat.nat Types.option) }
263 val prog_params_rect_Type4 :
264 (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
265 Types.option) -> 'a1) -> prog_params -> 'a1
267 val prog_params_rect_Type5 :
268 (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
269 Types.option) -> 'a1) -> prog_params -> 'a1
271 val prog_params_rect_Type3 :
272 (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
273 Types.option) -> 'a1) -> prog_params -> 'a1
275 val prog_params_rect_Type2 :
276 (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
277 Types.option) -> 'a1) -> prog_params -> 'a1
279 val prog_params_rect_Type1 :
280 (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
281 Types.option) -> 'a1) -> prog_params -> 'a1
283 val prog_params_rect_Type0 :
284 (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
285 Types.option) -> 'a1) -> prog_params -> 'a1
287 val prog_spars : prog_params -> Joint_semantics.sem_params
289 val prog : prog_params -> Joint.joint_program
291 val stack_sizes : prog_params -> AST.ident -> Nat.nat Types.option
293 val prog_params_inv_rect_Type4 :
294 prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
295 (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
297 val prog_params_inv_rect_Type3 :
298 prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
299 (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
301 val prog_params_inv_rect_Type2 :
302 prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
303 (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
305 val prog_params_inv_rect_Type1 :
306 prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
307 (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
309 val prog_params_inv_rect_Type0 :
310 prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
311 (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
313 val prog_params_jmdiscr : prog_params -> prog_params -> __
315 val prog_spars__o__spp' : prog_params -> Joint_semantics.serialized_params
317 val prog_spars__o__spp'__o__msu_pars :
318 prog_params -> Joint.joint_closed_internal_function
319 Joint_semantics.sem_unserialized_params
321 val prog_spars__o__spp'__o__msu_pars__o__st_pars :
322 prog_params -> Joint_semantics.sem_state_params
324 val prog_spars__o__spp'__o__spp : prog_params -> Joint.params
326 val prog_spars__o__spp'__o__spp__o__stmt_pars :
327 prog_params -> Joint.stmt_params
329 val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
330 prog_params -> Joint.uns_params
332 val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
333 prog_params -> Joint.unserialized_params
335 val joint_make_global : prog_params -> evaluation_params
337 val joint_make_global__o__ev_genv : prog_params -> Joint_semantics.genv
339 val joint_make_global__o__ev_genv__o__ge :
340 prog_params -> Joint.joint_closed_internal_function AST.fundef
343 val joint_make_global__o__ev_genv__o__ge__o__inject :
344 prog_params -> Joint.joint_closed_internal_function AST.fundef
345 Globalenvs.genv_t Types.sig0
347 val joint_make_global__o__ev_genv__o__inject :
348 prog_params -> Joint_semantics.genv Types.sig0
350 val joint_make_global__o__inject :
351 prog_params -> evaluation_params Types.sig0
353 val make_initial_state : prog_params -> Joint_semantics.state_pc Errors.res
355 val joint_classify_step :
356 Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
357 StructuredTraces.status_class
359 val joint_classify_final :
360 Joint.unserialized_params -> Joint.joint_fin_step ->
361 StructuredTraces.status_class
364 Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
365 -> StructuredTraces.status_class
367 val joint_call_ident :
368 Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
371 val joint_tailcall_ident :
372 Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
375 val pcDeq : Deqsets.deqSet
377 val cost_label_of_stmt :
378 Joint.stmt_params -> AST.ident List.list -> Joint.joint_statement ->
379 CostLabel.costlabel Types.option
381 val joint_label_of_pc :
382 Joint_semantics.sem_params -> evaluation_params ->
383 ByteValues.program_counter -> CostLabel.costlabel Types.option
385 val exit_pc' : ByteValues.program_counter
388 Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
389 -> Integers.int Types.option
391 val joint_abstract_status : prog_params -> StructuredTraces.abstract_status
394 Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
395 Types.option) -> StructuredTraces.abstract_status