source: src/Cminor/test/factorial.Cminor.ma @ 2183

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

definition label_of_nat : nat -> identifier Label := identifier_of_nat ?.



definition id_get_input := ident_of_nat 0.
definition f_get_input := External internal_function (mk_external_function id_get_input (mk_signature [] (Some ? (ASTint I32 Signed)))).
definition id_main := ident_of_nat 1.
definition id_main_i := ident_of_nat 7.
definition id_main_j := ident_of_nat 8.
definition id_main_r := ident_of_nat 9.
definition id_main__tmp0 := ident_of_nat 10.
definition C_cost2 := costlabel_of_nat 6.
definition L_tmp1 := label_of_nat 5.
definition C_cost0 := costlabel_of_nat 4.
definition L_tmp2 := label_of_nat 3.
definition C_cost1 := costlabel_of_nat 2.
definition f_main := Internal ? (mk_internal_function
  (Some ? (ASTint I32 Signed))
  []
  [mk_Prod ?? id_main_i (ASTint I32 Signed); mk_Prod ?? id_main_j (ASTint I32 Signed); mk_Prod ?? id_main_r (ASTint I32 Signed); mk_Prod ?? id_main__tmp0 (ASTint I32 Signed)]
  (match daemon in False with [ ])
0 (
  St_cost C_cost2 (
  St_seq (
    St_seq (
      St_call (Some ? (mk_Prod ?? id_main__tmp0 (ASTint I32 Signed))) (Cst ? (Oaddrsymbol id_get_input 0)) []
    ) (
    St_assign (ASTint I32 Signed) id_main_i (Id (ASTint I32 Signed) id_main__tmp0)
    )
  ) (
  St_seq (
    St_assign (ASTint I32 Signed) id_main_r (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))
  ) (
  St_seq (
    St_seq (
      St_seq (
        St_assign (ASTint I32 Signed) id_main_j (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 2))))
      ) (
      St_seq (
        St_label L_tmp1 (
        St_seq (
          St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cle) (Id (ASTint I32 Signed) id_main_j) (Id (ASTint I32 Signed) id_main_i)) (
            St_skip          ) (
            St_goto L_tmp2
          )
        ) (
        St_seq (
          St_seq (
            St_cost C_cost0 (
            St_assign (ASTint I32 Signed) id_main_r (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Id (ASTint I32 Signed) id_main_r) (Id (ASTint I32 Signed) id_main_j))
            )
          ) (
          St_assign (ASTint I32 Signed) id_main_j (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Oadd (Id (ASTint I32 Signed) id_main_j) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))
          )
        ) (
        St_goto L_tmp1
        )
        )
        )
      ) (
      St_label L_tmp2 (
      St_skip      )
      )
      )
    ) (
    St_cost C_cost1 (
    St_skip    )
    )
  ) (
  St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Id (ASTint I32 Signed) id_main_r)))
  )
  )
  )
  )

) (match daemon in False with [ ])).



definition myprog : Cminor_program :=
mk_program ?? [] [
  (mk_Prod ?? id_get_input f_get_input);
  (mk_Prod ?? id_main f_main)
]  id_main
.