101 open Hints_declaration
117 open Cminor_semantics
127 (** val cminor_stack_ident :
128 Cminor_semantics.genv -> Cminor_abstract.cminor_state -> AST.ident **)
129 let cminor_stack_ident ge s =
131 | Cminor_semantics.State (x, x0, x1, x4, x5, x6, x8) ->
132 (fun _ -> assert false (* absurd case *))
133 | Cminor_semantics.Callstate (id, x, x0, x1, x2) -> (fun _ -> id)
134 | Cminor_semantics.Returnstate (x, x0, x1) ->
135 (fun _ -> assert false (* absurd case *))
136 | Cminor_semantics.Finalstate x ->
137 (fun _ -> assert false (* absurd case *))) __
139 (** val cminor_pcs : Measurable.preclassified_system **)
141 { Measurable.pcs_exec = Cminor_semantics.cminor_fullexec;
142 Measurable.pcs_labelled = (fun x ->
143 Obj.magic Cminor_abstract.cminor_labelled); Measurable.pcs_classify =
144 (fun x -> Obj.magic Cminor_abstract.cminor_classify);
145 Measurable.pcs_callee =
146 (Obj.magic (fun x x0 _ -> cminor_stack_ident x x0)) }