source: src/Cminor/test/null-op.ma @ 879

include "Cminor/semantics.ma".
include "common/Animation.ma".

(* NB: I've had to add Optrofint in a couple of places because the prototype
       isn't handling conversions between zero and null pointers at the moment.
       *)

definition id_main := ident_of_nat 0.
definition id_main_tmp0 := ident_of_nat 6.
definition id_main_q := ident_of_nat 7.
definition id_main_p := ident_of_nat 8.
definition id_main_c := ident_of_nat 9.
definition C_cost4 := costlabel_of_nat 5.
definition C_cost2 := costlabel_of_nat 4.
definition C_cost3 := costlabel_of_nat 3.
definition C_cost0 := costlabel_of_nat 2.
definition C_cost1 := costlabel_of_nat 1.
definition f_main := Internal ? (mk_internal_function
  (mk_signature [] (Some ? (ASTint I32 Signed)))
  []
  [id_main_tmp0; id_main_q; id_main_p; id_main_c]
  [id_main_q; id_main_p]
  1 (
  St_cost C_cost4 (
  St_seq (
    St_assign id_main_p (Op1 (Optrofint Any) (Cst (Ointconst (repr 0))))
  ) (
  St_seq (
    St_assign id_main_q (Cst (Oaddrstack (repr 0)))
  ) (
  St_seq (
    St_ifthenelse (Op2 (Ocmpp Ceq) (Id id_main_p) (Id id_main_q)) (
      St_cost C_cost2 (
      St_return (Some ? (Cst (Ointconst (repr 0))))
      )
    ) (
      St_cost C_cost3 (
      St_skip      )
    )
  ) (
  St_seq (
    St_ifthenelse (Op2 (Ocmp Cgt) (Op2 Osubpp (Id id_main_p) (Id id_main_p)) (Cst (Ointconst (repr 0)))) (
      St_cost C_cost0 (
      St_return (Some ? (Cst (Ointconst (repr 0))))
      )
    ) (
      St_cost C_cost1 (
      St_skip      )
    )
  ) (
  St_seq (
    St_assign id_main_p (Op2 Oaddp (Id id_main_p) (Op2 Omul (Cst (Ointconst (repr 0))) (Cst (Ointconst (repr 1)))))
  ) (
  St_seq (
    St_assign id_main_p (Op2 Oaddp (Id id_main_p) (Op2 Omul (Cst (Ointconst (repr 0))) (Cst (Ointconst (repr 1)))))
  ) (
  St_seq (
    St_assign id_main_p (Op2 Osubpi (Id id_main_p) (Op2 Omul (Cst (Ointconst (repr 0))) (Cst (Ointconst (repr 1)))))
  ) (
  St_return (Some ? (Op2 (Ocmpp Ceq) (Id id_main_p) (Op1 (Optrofint Any) (Cst (Ointconst (repr 0))))))
  )
  )
  )
  )
  )
  )
  )
  )

)).



definition myprog : Cminor_program :=
mk_program ?? [
  (pair ?? id_main f_main)
]  id_main
[]
.

example exec: finishes_with (repr 1) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
normalize  (* you can examine the result here *)
@refl
qed.

include "Cminor/toRTLabs.ma".
include "RTLabs/semantics.ma".

example execRTL: finishes_with (repr 1) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
normalize  (* you can examine the result here *)
@refl
qed.