include "Clight/Cexec.ma".
include "common/Animation.ma".

definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
  [][〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
    〈ident_of_nat 1 (* main *), CL_Internal (
      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ; 〈ident_of_nat 4, (Tint I32 Signed  )〉 ]
        (Ssequence
        (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
          (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed  )))
          [])
        (Ssequence
        (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
          (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
        (Ssequence
        (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
                (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
          (Expr (Ebinop Ole
            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
            (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
            (Tint I32 Signed  ))
          (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
            (Expr (Ebinop Oadd
              (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
              (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
              (Tint I32 Signed  )))
          (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
            (Expr (Ebinop Omul
              (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
              (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  )))
              (Tint I32 Signed  )))
        )
        (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
                              (Tint I32 Signed  )))))))
      
      
      
    )〉]
  (ident_of_nat 1)
  
.

(*
example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
normalize  (* you can examine the result here *)
*)