source: src/Cminor/test/sum.ma @ 882

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

definition id_src := ident_of_nat 7.


definition id_main := ident_of_nat 0.
definition id_main_tmp0 := ident_of_nat 4.
definition id_main_total := ident_of_nat 5.
definition id_main_i := ident_of_nat 6.
definition C_cost2 := 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_total; id_main_i]
  []
  0 (
  St_cost C_cost2 (
  St_seq (
    St_assign id_main_total (Cst (Ointconst (repr 0)))
  ) (
  St_seq (
    St_seq (
      St_seq (
        St_assign id_main_i (Cst (Ointconst (repr 0)))
      ) (
      St_block (
        St_loop (
          St_seq (
            St_ifthenelse (Op1 Onotbool (Op2 (Ocmpu Clt) (Id id_main_i) (Cst (Ointconst (repr 5))))) (
              St_exit 0
            ) (
              St_skip            )
          ) (
          St_seq (
            St_block (
              St_cost C_cost0 (
              St_assign id_main_total (Op2 Oadd (Op1 Ocast8unsigned (Id id_main_total)) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Cst (Oaddrsymbol id_src (repr 0))) (Op2 Omul (Id id_main_i) (Cst (Ointconst (repr 1))))))))
              )
            )
          ) (
          St_assign id_main_i (Op2 Oadd (Id id_main_i) (Cst (Ointconst (repr 1))))
          )
          )
        )
      )
      )
    ) (
    St_cost C_cost1 (
    St_skip    )
    )
  ) (
  St_return (Some ? (Op1 Ocast8unsigned (Id id_main_total)))
  )
  )
  )

)).



definition myprog : Cminor_program :=
mk_program ?? [
  (pair ?? id_main f_main)
]  id_main
[(pair ?? (pair ?? (pair ?? id_src [Init_int8 (repr 28);Init_int8 (repr 17);Init_int8 (repr 17);Init_int8 (repr 8);Init_int8 (repr 4)]) Any) it)]
.

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

include "Cminor/initialisation.ma".

example exec2: finishes_with (repr 74) ? (exec_up_to Cminor_fullexec (replace_init myprog) 1000 [ ]).
normalize in ⊢ (???(??%??)) (* examine the program here *)
normalize  (* you can examine the result here *)
@refl
qed.

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

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