117 open Hints_declaration
129 open RTLabs_semantics
139 (** val rTLabs_stack_ident :
140 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_state -> AST.ident **)
141 let rTLabs_stack_ident ge s =
143 | RTLabs_semantics.State (x, x0, x1) ->
144 (fun _ -> assert false (* absurd case *))
145 | RTLabs_semantics.Callstate (id, x, x0, x1, x2, x3) -> (fun _ -> id)
146 | RTLabs_semantics.Returnstate (x, x0, x1, x2) ->
147 (fun _ -> assert false (* absurd case *))
148 | RTLabs_semantics.Finalstate x ->
149 (fun _ -> assert false (* absurd case *))) __
151 (** val rTLabs_pcs : Measurable.preclassified_system **)
153 { Measurable.pcs_exec = RTLabs_semantics.rTLabs_fullexec;
154 Measurable.pcs_labelled = (fun x ->
155 Obj.magic RTLabs_abstract.rTLabs_cost); Measurable.pcs_classify =
156 (fun x -> Obj.magic RTLabs_abstract.rTLabs_classify);
157 Measurable.pcs_callee =
158 (Obj.magic (fun x x0 _ -> rTLabs_stack_ident x x0)) }
160 (** val rTLabs_ext_pcs : Measurable.preclassified_system **)
162 { Measurable.pcs_exec = RTLabs_abstract.rTLabs_ext_fullexec;
163 Measurable.pcs_labelled = (fun g s ->
164 RTLabs_abstract.rTLabs_cost (Obj.magic s).RTLabs_abstract.ras_state);
165 Measurable.pcs_classify = (fun g s ->
166 RTLabs_abstract.rTLabs_classify (Obj.magic s).RTLabs_abstract.ras_state);
167 Measurable.pcs_callee = (fun g s _ ->
168 rTLabs_stack_ident (Obj.magic g) (Obj.magic s).RTLabs_abstract.ras_state) }