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

definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
  [][〈ident_of_nat 0 (* main *), CL_Internal (
       mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I8 Unsigned ))〉 ]
         (Ssequence
         (Sassign (Expr (Evar (ident_of_nat 2))
                    (Tpointer Any (Tint I8 Unsigned )))
           (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
             (Tpointer Any (Tint I8 Unsigned ))))
         (Ssequence
         (Sassign (Expr (Evar (ident_of_nat 3))
                    (Tpointer Any (Tint I8 Unsigned )))
           (Expr (Eaddrof (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
             (Tpointer Any (Tint I8 Unsigned ))))
         (Ssequence
         (Sifthenelse (Expr (Ebinop Oeq
                        (Expr (Evar (ident_of_nat 2))
                          (Tpointer Any (Tint I8 Unsigned )))
                        (Expr (Evar (ident_of_nat 3))
                          (Tpointer Any (Tint I8 Unsigned ))))
                        (Tint I32 Signed  ))
           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
                                 (Tint I32 Signed  ))))
           Sskip)
         (Ssequence
         (Sifthenelse (Expr (Ebinop Ogt
                        (Expr (Ebinop Osub
                          (Expr (Evar (ident_of_nat 2))
                            (Tpointer Any (Tint I8 Unsigned )))
                          (Expr (Evar (ident_of_nat 2))
                            (Tpointer Any (Tint I8 Unsigned ))))
                          (Tint I32 Signed  ))
                        (Expr (Econst_int I32 (repr ? 0))
                          (Tint I32 Signed  ))) (Tint I32 Signed  ))
           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
                                 (Tint I32 Signed  ))))
           Sskip)
         (Ssequence
         (Sassign (Expr (Evar (ident_of_nat 2))
                    (Tpointer Any (Tint I8 Unsigned )))
           (Expr (Ebinop Oadd
             (Expr (Evar (ident_of_nat 2))
               (Tpointer Any (Tint I8 Unsigned )))
             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
             (Tpointer Any (Tint I8 Unsigned ))))
         (Ssequence
         (Sassign (Expr (Evar (ident_of_nat 2))
                    (Tpointer Any (Tint I8 Unsigned )))
           (Expr (Ebinop Oadd
             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  ))
             (Expr (Evar (ident_of_nat 2))
               (Tpointer Any (Tint I8 Unsigned ))))
             (Tpointer Any (Tint I8 Unsigned ))))
         (Ssequence
         (Sassign (Expr (Evar (ident_of_nat 2))
                    (Tpointer Any (Tint I8 Unsigned )))
           (Expr (Ebinop Osub
             (Expr (Evar (ident_of_nat 2))
               (Tpointer Any (Tint I8 Unsigned )))
             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
             (Tpointer Any (Tint I8 Unsigned ))))
         (Sreturn (Some expr (Expr (Ebinop Oeq
                               (Expr (Evar (ident_of_nat 2))
                                 (Tpointer Any (Tint I8 Unsigned )))
                               (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
                                 (Expr (Ecast (Tpointer Any Tvoid)
                                   (Expr (Econst_int I8 (repr ? 0))
                                     (Tint I8 Unsigned )))
                                   (Tpointer Any Tvoid)))
                                 (Tpointer Any (Tint I8 Unsigned ))))
                               (Tint I32 Signed  )))))))))))
       
       
       
     )〉]
  (ident_of_nat 0)
  
.

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