Library compcert.cfrontend.CexecImpl

Require Cexec.
Require EventsImpl.


Definition do_initial_state := Cexec.do_initial_state (mem := Memimpl.mem).
Definition do_step := Cexec.do_step (mem := Memimpl.mem).
Definition step_expr := Cexec.step_expr (mem := Memimpl.mem).
Definition at_final_state := Cexec.at_final_state (mem := Memimpl.mem).