105 open Hints_declaration
133 (** val clight_stack_ident :
134 Clight_abstract.cl_genv -> Clight_abstract.clight_state -> AST.ident **)
135 let clight_stack_ident ge s =
137 | Csem.State (x, x0, x1, x2, x3) ->
138 (fun _ -> assert false (* absurd case *))
139 | Csem.Callstate (id, x, x0, x1, x2) -> (fun _ -> id)
140 | Csem.Returnstate (x, x0, x1) ->
141 (fun _ -> assert false (* absurd case *))
142 | Csem.Finalstate x -> (fun _ -> assert false (* absurd case *))) __
144 (** val clight_pcs : Measurable.preclassified_system **)
146 { Measurable.pcs_exec = Cexec.clight_fullexec; Measurable.pcs_labelled =
147 (fun x -> Obj.magic Clight_abstract.clight_labelled);
148 Measurable.pcs_classify = (fun x ->
149 Obj.magic Clight_abstract.clight_classify); Measurable.pcs_callee =
150 (Obj.magic (fun x x0 _ -> clight_stack_ident x x0)) }