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

definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
  [〈〈ident_of_nat 0 (* src *), Any〉,
     〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
        (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
        (Init_int8 (repr I8 4)) ], (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
  [〈ident_of_nat 1 (* main *), CL_Internal (
     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
       (Ssequence
       (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
         (Expr (Ecast (Tint I8 Unsigned )
           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
           (Tint I8 Unsigned )))
       (Ssequence
       (Sfor (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
               (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
         (Expr (Ebinop Olt
           (Expr (Ecast (Tint I32 Unsigned)
             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
             (Tint I32 Unsigned))
           (Expr (Esizeof (Tarray Any (Tint I8 Unsigned ) 5))
             (Tint I32 Unsigned))) (Tint I32 Signed  ))
         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
           (Expr (Ebinop Oadd
             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
             (Tint I32 Signed  )))
         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
           (Expr (Ecast (Tint I8 Unsigned )
             (Expr (Ebinop Oadd
               (Expr (Ecast (Tint I32 Signed  )
                 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
                 (Tint I32 Signed  ))
               (Expr (Ecast (Tint I32 Signed  )
                 (Expr (Ederef
                   (Expr (Ebinop Oadd
                     (Expr (Evar (ident_of_nat 0))
                       (Tarray Any (Tint I8 Unsigned ) 5))
                     (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
                     (Tpointer Any (Tint I8 Unsigned ))))
                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
               (Tint I32 Signed  ))) (Tint I8 Unsigned )))
       )
       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
                             (Expr (Evar (ident_of_nat 3))
                               (Tint I8 Unsigned ))) (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 *)
*)