135 open Hints_declaration
164 Joint_semantics.sem_params -> (IO.io_out, IO.io_in)
165 SmallstepExec.trans_system **)
167 { SmallstepExec.is_final = (fun env ->
168 Obj.magic (Traces.joint_final g (Obj.magic env))); SmallstepExec.step =
171 (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
173 (Joint_semantics.eval_state g (Obj.magic env).Traces.globals
174 (Obj.magic env).Traces.ev_genv (Obj.magic st))) (fun st' ->
176 match Traces.joint_label_of_pc g (Obj.magic env)
177 (Obj.magic st).Joint_semantics.pc with
178 | Types.None -> Events.e0
179 | Types.Some c -> Events.echarge c
181 Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = charge;
182 Types.snd = st' }))) }
184 (** val joint_fullexec :
185 Joint_semantics.sem_params -> (IO.io_out, IO.io_in)
186 SmallstepExec.fullexec **)
187 let joint_fullexec g =
188 { SmallstepExec.es1 = (joint_exec g); SmallstepExec.make_global =
191 (Traces.joint_make_global { Traces.prog_spars = g; Traces.prog =
192 (Obj.magic pr).Types.fst; Traces.stack_sizes =
193 (Obj.magic pr).Types.snd })); SmallstepExec.make_initial_state =
196 (Traces.make_initial_state { Traces.prog_spars = g; Traces.prog =
197 (Obj.magic p_stacks).Types.fst; Traces.stack_sizes =
198 (Obj.magic p_stacks).Types.snd })) }
200 (** val joint_preclassified_system :
201 Joint_semantics.sem_params -> Measurable.preclassified_system **)
202 let joint_preclassified_system g =
203 { Measurable.pcs_exec = (joint_fullexec g); Measurable.pcs_labelled =
207 (Traces.joint_label_of_pc g (Obj.magic env)
208 (Obj.magic st).Joint_semantics.pc))); Measurable.pcs_classify =
209 (fun env -> Obj.magic (Traces.joint_classify g (Obj.magic env)));
210 Measurable.pcs_callee = (fun env s _ ->
211 Traces.joint_call_ident g (Obj.magic env) (Obj.magic s)) }