(* NB: this was produced via compcert, acc and some hand mangling because acc
       doesn't yet implement switch correctly in the clight → cminor phase. *)

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

definition id_get := ident_of_nat 99.
definition f_get := External internal_function (mk_external_function id_get (mk_signature [] (Some ? (ASTint I32 Signed)))).


definition id_main := ident_of_nat 0.
definition id_main_i := ident_of_nat 1.
definition id_main_x1 := ident_of_nat 2.
definition f_main := Internal ? (mk_internal_function
  (mk_signature [] (Some ? (ASTint I32 Signed)))
  []
  [id_main_i; id_main_x1]
  []
  0 (
  St_seq (
    St_assign id_main_i (Op1 Ocast8unsigned (Cst (Ointconst (repr 0))))
  ) (
  St_seq (
    St_call (Some ? id_main_x1) (Cst (Oaddrsymbol id_get zero)) []
  ) (
  St_seq (
    St_block (
      St_seq (
        St_block (
          St_seq (
            St_block (
              St_seq (
                St_block (
                  St_seq (
                    St_block (
                      St_seq (
                        St_block (
                          St_seq (
                            St_switch (Id id_main_x1) [
                              (pair ?? (repr 1) 0);
                              (pair ?? (repr 3) 1);
                              (pair ?? (repr 5) 2);
                              (pair ?? (repr 7) 3)] 4
                          ) (
                          St_skip                          )
                        )
                      ) (
                      St_seq (
                        St_exit 4
                      ) (
                      St_skip                      )
                      )
                    )
                  ) (
                  St_seq (
                    St_assign id_main_i (Op1 Ocast8unsigned (Op2 Oadd (Id id_main_i) (Cst (Ointconst (repr 1)))))
                  ) (
                  St_seq (
                    St_exit 3
                  ) (
                  St_skip                  )
                  )
                  )
                )
              ) (
              St_seq (
                St_assign id_main_i (Op1 Ocast8unsigned (Op2 Oadd (Id id_main_i) (Cst (Ointconst (repr 2)))))
              ) (
              St_skip              )
              )
            )
          ) (
          St_seq (
            St_assign id_main_i (Op1 Ocast8unsigned (Op2 Oadd (Id id_main_i) (Cst (Ointconst (repr 3)))))
          ) (
          St_seq (
            St_exit 1
          ) (
          St_skip          )
          )
          )
        )
      ) (
      St_seq (
        St_assign id_main_i (Op1 Ocast8unsigned (Op2 Oadd (Id id_main_i) (Cst (Ointconst (repr 16)))))
      ) (
      St_skip      )
      )
    )
  ) (
  St_seq (
    St_return (Some ? (Id id_main_i))
  ) (
  St_skip  )
  )
  )
  )

)).



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


example exec0: finishes_with (repr 16) ? (exec_up_to Cminor_fullexec myprog 100 [EVint (repr 0)]).
normalize  (* you can examine the result here *)
@refl qed.

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

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

example exec5: finishes_with (repr 5) ? (exec_up_to Cminor_fullexec myprog 100 [EVint (repr 5)]).
normalize  (* you can examine the result here *)
@refl qed.

example exec7: finishes_with (repr 3) ? (exec_up_to Cminor_fullexec myprog 100 [EVint (repr 7)]).
normalize  (* you can examine the result here *)
@refl qed.

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

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

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

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

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

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