Require Import Common.
Require Import ValuesNTypes.
Require Import ProgramStructures.
Require Import Heap.
Require Import ZArith.
Require Import Program.
Require Import RuntimeStructures.
Require Import Semantics.
Require Import ArithOps.
Require Import List.
Require Import Relations.
Import List.ListNotations.

Declare Module P : PROGRAM_W_CONSTRUCTORS.
Module PS := P.M_ProgramStructures.
Module VAT := PS.M_ValuesAndTypes.
Module INum := VAT.M_Numeric_Int.
Module PSFacts := ProgramStructuresFacts PS.

Import P PS PSFacts VAT.

Parameter n: Z.


Definition A_m_code: P.TCode := P.codeFromList
  [ I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.zero))));
    I_Frame (FI_Var (VI_Store VIKInt var0));
    I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.const 50))));
    I_Frame (FI_Var (VI_Store VIKInt var1));
    I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.zero))));
    I_Frame (FI_Var (VI_Store VIKInt var2));
    I_Frame (FI_Var (VI_Load VIKInt var0));
    I_Frame (FI_Var (VI_Load VIKInt var1));
    I_Frame (FI_Cond (CI_Cmp KInt ArithmeticOperators.CmpOp_ge (offsetFromPosition 19%nat)));
    I_Frame (FI_Var (VI_Load VIKInt var0));
    I_Frame (FI_Var (VI_Load VIKInt var2));
    I_Frame (FI_Stackop (SI_Binop KInt ArithmeticOperators.BinOp_add));
    I_Frame (FI_Var (VI_Store VIKInt var2));
    I_Frame (FI_Var (VI_Inc var0 (INum.one)));
    I_Frame (FI_Var (VI_Load VIKInt var0));
    I_Frame (FI_Var (VI_Load VIKInt var2));
    I_Frame (FI_Stackop (SI_Binop KInt ArithmeticOperators.BinOp_add));
    I_Frame (FI_Var (VI_Store VIKInt var2));
    I_Frame (FI_Cond (CI_Goto (offsetFromPosition 6%nat)));
    I_Frame (FI_Var (VI_Load VIKInt var2));
    I_Return (Some KInt)
  ].