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

definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
  [][〈ident_of_nat 0 (* copy *), CL_Internal (
       mk_function Tvoid [〈ident_of_nat 19, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 20, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed  )〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 4, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 7, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 8, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 10, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 11, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 12, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 14, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 15, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 17, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 18, (Tpointer Any (Tint I16 Signed  ))〉 ]
         (Ssequence
         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
           (Expr (Ebinop Odiv
             (Expr (Ebinop Oadd
               (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed  ))
               (Expr (Econst_int I32 (repr ? 7)) (Tint I32 Signed  )))
               (Tint I32 Signed  ))
             (Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed  )))
             (Tint I32 Signed  )))
         (Sswitch (Expr (Ebinop Omod
                    (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed  ))
                    (Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed  )))
                    (Tint I32 Signed  )) (
           (LScase I32 (repr ? 0)
             (Slabel (ident_of_nat 22)
             (Ssequence
             (Ssequence
             (Sassign (Expr (Evar (ident_of_nat 17))
                        (Tpointer Any (Tint I16 Signed  )))
               (Expr (Evar (ident_of_nat 19))
                 (Tpointer Any (Tint I16 Signed  ))))
             (Sassign (Expr (Evar (ident_of_nat 19))
                        (Tpointer Any (Tint I16 Signed  )))
               (Expr (Ebinop Oadd
                 (Expr (Evar (ident_of_nat 17))
                   (Tpointer Any (Tint I16 Signed  )))
                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
                 (Tpointer Any (Tint I16 Signed  )))))
             (Ssequence
             (Ssequence
             (Sassign (Expr (Evar (ident_of_nat 18))
                        (Tpointer Any (Tint I16 Signed  )))
               (Expr (Evar (ident_of_nat 20))
                 (Tpointer Any (Tint I16 Signed  ))))
             (Sassign (Expr (Evar (ident_of_nat 20))
                        (Tpointer Any (Tint I16 Signed  )))
               (Expr (Ebinop Oadd
                 (Expr (Evar (ident_of_nat 18))
                   (Tpointer Any (Tint I16 Signed  )))
                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
                 (Tpointer Any (Tint I16 Signed  )))))
             (Sassign (Expr (Ederef
                        (Expr (Evar (ident_of_nat 17))
                          (Tpointer Any (Tint I16 Signed  ))))
                        (Tint I16 Signed  ))
               (Expr (Ederef
                 (Expr (Evar (ident_of_nat 18))
                   (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
             (LScase I32 (repr ? 7)
               (Ssequence
               (Sassign (Expr (Evar (ident_of_nat 15))
                          (Tpointer Any (Tint I16 Signed  )))
                 (Expr (Evar (ident_of_nat 19))
                   (Tpointer Any (Tint I16 Signed  ))))
               (Ssequence
               (Sassign (Expr (Evar (ident_of_nat 19))
                          (Tpointer Any (Tint I16 Signed  )))
                 (Expr (Ebinop Oadd
                   (Expr (Evar (ident_of_nat 15))
                     (Tpointer Any (Tint I16 Signed  )))
                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
                   (Tpointer Any (Tint I16 Signed  ))))
               (Ssequence
               (Sassign (Expr (Evar (ident_of_nat 16))
                          (Tpointer Any (Tint I16 Signed  )))
                 (Expr (Evar (ident_of_nat 20))
                   (Tpointer Any (Tint I16 Signed  ))))
               (Ssequence
               (Sassign (Expr (Evar (ident_of_nat 20))
                          (Tpointer Any (Tint I16 Signed  )))
                 (Expr (Ebinop Oadd
                   (Expr (Evar (ident_of_nat 16))
                     (Tpointer Any (Tint I16 Signed  )))
                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
                   (Tpointer Any (Tint I16 Signed  ))))
               (Sassign (Expr (Ederef
                          (Expr (Evar (ident_of_nat 15))
                            (Tpointer Any (Tint I16 Signed  ))))
                          (Tint I16 Signed  ))
                 (Expr (Ederef
                   (Expr (Evar (ident_of_nat 16))
                     (Tpointer Any (Tint I16 Signed  ))))
                   (Tint I16 Signed  )))))))
               (LScase I32 (repr ? 6)
                 (Ssequence
                 (Sassign (Expr (Evar (ident_of_nat 13))
                            (Tpointer Any (Tint I16 Signed  )))
                   (Expr (Evar (ident_of_nat 19))
                     (Tpointer Any (Tint I16 Signed  ))))
                 (Ssequence
                 (Sassign (Expr (Evar (ident_of_nat 19))
                            (Tpointer Any (Tint I16 Signed  )))
                   (Expr (Ebinop Oadd
                     (Expr (Evar (ident_of_nat 13))
                       (Tpointer Any (Tint I16 Signed  )))
                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
                     (Tpointer Any (Tint I16 Signed  ))))
                 (Ssequence
                 (Sassign (Expr (Evar (ident_of_nat 14))
                            (Tpointer Any (Tint I16 Signed  )))
                   (Expr (Evar (ident_of_nat 20))
                     (Tpointer Any (Tint I16 Signed  ))))
                 (Ssequence
                 (Sassign (Expr (Evar (ident_of_nat 20))
                            (Tpointer Any (Tint I16 Signed  )))
                   (Expr (Ebinop Oadd
                     (Expr (Evar (ident_of_nat 14))
                       (Tpointer Any (Tint I16 Signed  )))
                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
                     (Tpointer Any (Tint I16 Signed  ))))
                 (Sassign (Expr (Ederef
                            (Expr (Evar (ident_of_nat 13))
                              (Tpointer Any (Tint I16 Signed  ))))
                            (Tint I16 Signed  ))
                   (Expr (Ederef
                     (Expr (Evar (ident_of_nat 14))
                       (Tpointer Any (Tint I16 Signed  ))))
                     (Tint I16 Signed  )))))))
                 (LScase I32 (repr ? 5)
                   (Ssequence
                   (Sassign (Expr (Evar (ident_of_nat 11))
                              (Tpointer Any (Tint I16 Signed  )))
                     (Expr (Evar (ident_of_nat 19))
                       (Tpointer Any (Tint I16 Signed  ))))
                   (Ssequence
                   (Sassign (Expr (Evar (ident_of_nat 19))
                              (Tpointer Any (Tint I16 Signed  )))
                     (Expr (Ebinop Oadd
                       (Expr (Evar (ident_of_nat 11))
                         (Tpointer Any (Tint I16 Signed  )))
                       (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
                       (Tpointer Any (Tint I16 Signed  ))))
                   (Ssequence
                   (Sassign (Expr (Evar (ident_of_nat 12))
                              (Tpointer Any (Tint I16 Signed  )))
                     (Expr (Evar (ident_of_nat 20))
                       (Tpointer Any (Tint I16 Signed  ))))
                   (Ssequence
                   (Sassign (Expr (Evar (ident_of_nat 20))
                              (Tpointer Any (Tint I16 Signed  )))
                     (Expr (Ebinop Oadd
                       (Expr (Evar (ident_of_nat 12))
                         (Tpointer Any (Tint I16 Signed  )))
                       (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
                       (Tpointer Any (Tint I16 Signed  ))))
                   (Sassign (Expr (Ederef
                              (Expr (Evar (ident_of_nat 11))
                                (Tpointer Any (Tint I16 Signed  ))))
                              (Tint I16 Signed  ))
                     (Expr (Ederef
                       (Expr (Evar (ident_of_nat 12))
                         (Tpointer Any (Tint I16 Signed  ))))
                       (Tint I16 Signed  )))))))
                   (LScase I32 (repr ? 4)
                     (Ssequence
                     (Sassign (Expr (Evar (ident_of_nat 9))
                                (Tpointer Any (Tint I16 Signed  )))
                       (Expr (Evar (ident_of_nat 19))
                         (Tpointer Any (Tint I16 Signed  ))))
                     (Ssequence
                     (Sassign (Expr (Evar (ident_of_nat 19))
                                (Tpointer Any (Tint I16 Signed  )))
                       (Expr (Ebinop Oadd
                         (Expr (Evar (ident_of_nat 9))
                           (Tpointer Any (Tint I16 Signed  )))
                         (Expr (Econst_int I32 (repr ? 1))
                           (Tint I32 Signed  )))
                         (Tpointer Any (Tint I16 Signed  ))))
                     (Ssequence
                     (Sassign (Expr (Evar (ident_of_nat 10))
                                (Tpointer Any (Tint I16 Signed  )))
                       (Expr (Evar (ident_of_nat 20))
                         (Tpointer Any (Tint I16 Signed  ))))
                     (Ssequence
                     (Sassign (Expr (Evar (ident_of_nat 20))
                                (Tpointer Any (Tint I16 Signed  )))
                       (Expr (Ebinop Oadd
                         (Expr (Evar (ident_of_nat 10))
                           (Tpointer Any (Tint I16 Signed  )))
                         (Expr (Econst_int I32 (repr ? 1))
                           (Tint I32 Signed  )))
                         (Tpointer Any (Tint I16 Signed  ))))
                     (Sassign (Expr (Ederef
                                (Expr (Evar (ident_of_nat 9))
                                  (Tpointer Any (Tint I16 Signed  ))))
                                (Tint I16 Signed  ))
                       (Expr (Ederef
                         (Expr (Evar (ident_of_nat 10))
                           (Tpointer Any (Tint I16 Signed  ))))
                         (Tint I16 Signed  )))))))
                     (LScase I32 (repr ? 3)
                       (Ssequence
                       (Sassign (Expr (Evar (ident_of_nat 7))
                                  (Tpointer Any (Tint I16 Signed  )))
                         (Expr (Evar (ident_of_nat 19))
                           (Tpointer Any (Tint I16 Signed  ))))
                       (Ssequence
                       (Sassign (Expr (Evar (ident_of_nat 19))
                                  (Tpointer Any (Tint I16 Signed  )))
                         (Expr (Ebinop Oadd
                           (Expr (Evar (ident_of_nat 7))
                             (Tpointer Any (Tint I16 Signed  )))
                           (Expr (Econst_int I32 (repr ? 1))
                             (Tint I32 Signed  )))
                           (Tpointer Any (Tint I16 Signed  ))))
                       (Ssequence
                       (Sassign (Expr (Evar (ident_of_nat 8))
                                  (Tpointer Any (Tint I16 Signed  )))
                         (Expr (Evar (ident_of_nat 20))
                           (Tpointer Any (Tint I16 Signed  ))))
                       (Ssequence
                       (Sassign (Expr (Evar (ident_of_nat 20))
                                  (Tpointer Any (Tint I16 Signed  )))
                         (Expr (Ebinop Oadd
                           (Expr (Evar (ident_of_nat 8))
                             (Tpointer Any (Tint I16 Signed  )))
                           (Expr (Econst_int I32 (repr ? 1))
                             (Tint I32 Signed  )))
                           (Tpointer Any (Tint I16 Signed  ))))
                       (Sassign (Expr (Ederef
                                  (Expr (Evar (ident_of_nat 7))
                                    (Tpointer Any (Tint I16 Signed  ))))
                                  (Tint I16 Signed  ))
                         (Expr (Ederef
                           (Expr (Evar (ident_of_nat 8))
                             (Tpointer Any (Tint I16 Signed  ))))
                           (Tint I16 Signed  )))))))
                       (LScase I32 (repr ? 2)
                         (Ssequence
                         (Sassign (Expr (Evar (ident_of_nat 5))
                                    (Tpointer Any (Tint I16 Signed  )))
                           (Expr (Evar (ident_of_nat 19))
                             (Tpointer Any (Tint I16 Signed  ))))
                         (Ssequence
                         (Sassign (Expr (Evar (ident_of_nat 19))
                                    (Tpointer Any (Tint I16 Signed  )))
                           (Expr (Ebinop Oadd
                             (Expr (Evar (ident_of_nat 5))
                               (Tpointer Any (Tint I16 Signed  )))
                             (Expr (Econst_int I32 (repr ? 1))
                               (Tint I32 Signed  )))
                             (Tpointer Any (Tint I16 Signed  ))))
                         (Ssequence
                         (Sassign (Expr (Evar (ident_of_nat 6))
                                    (Tpointer Any (Tint I16 Signed  )))
                           (Expr (Evar (ident_of_nat 20))
                             (Tpointer Any (Tint I16 Signed  ))))
                         (Ssequence
                         (Sassign (Expr (Evar (ident_of_nat 20))
                                    (Tpointer Any (Tint I16 Signed  )))
                           (Expr (Ebinop Oadd
                             (Expr (Evar (ident_of_nat 6))
                               (Tpointer Any (Tint I16 Signed  )))
                             (Expr (Econst_int I32 (repr ? 1))
                               (Tint I32 Signed  )))
                             (Tpointer Any (Tint I16 Signed  ))))
                         (Sassign (Expr (Ederef
                                    (Expr (Evar (ident_of_nat 5))
                                      (Tpointer Any (Tint I16 Signed  ))))
                                    (Tint I16 Signed  ))
                           (Expr (Ederef
                             (Expr (Evar (ident_of_nat 6))
                               (Tpointer Any (Tint I16 Signed  ))))
                             (Tint I16 Signed  )))))))
                         (LScase I32 (repr ? 1)
                           (Ssequence
                           (Sassign (Expr (Evar (ident_of_nat 3))
                                      (Tpointer Any (Tint I16 Signed  )))
                             (Expr (Evar (ident_of_nat 19))
                               (Tpointer Any (Tint I16 Signed  ))))
                           (Ssequence
                           (Sassign (Expr (Evar (ident_of_nat 19))
                                      (Tpointer Any (Tint I16 Signed  )))
                             (Expr (Ebinop Oadd
                               (Expr (Evar (ident_of_nat 3))
                                 (Tpointer Any (Tint I16 Signed  )))
                               (Expr (Econst_int I32 (repr ? 1))
                                 (Tint I32 Signed  )))
                               (Tpointer Any (Tint I16 Signed  ))))
                           (Ssequence
                           (Sassign (Expr (Evar (ident_of_nat 4))
                                      (Tpointer Any (Tint I16 Signed  )))
                             (Expr (Evar (ident_of_nat 20))
                               (Tpointer Any (Tint I16 Signed  ))))
                           (Ssequence
                           (Sassign (Expr (Evar (ident_of_nat 20))
                                      (Tpointer Any (Tint I16 Signed  )))
                             (Expr (Ebinop Oadd
                               (Expr (Evar (ident_of_nat 4))
                                 (Tpointer Any (Tint I16 Signed  )))
                               (Expr (Econst_int I32 (repr ? 1))
                                 (Tint I32 Signed  )))
                               (Tpointer Any (Tint I16 Signed  ))))
                           (Ssequence
                           (Sassign (Expr (Ederef
                                      (Expr (Evar (ident_of_nat 3))
                                        (Tpointer Any (Tint I16 Signed  ))))
                                      (Tint I16 Signed  ))
                             (Expr (Ederef
                               (Expr (Evar (ident_of_nat 4))
                                 (Tpointer Any (Tint I16 Signed  ))))
                               (Tint I16 Signed  )))
                           (Ssequence
                           (Sassign (Expr (Evar (ident_of_nat 2))
                                      (Tint I32 Signed  ))
                             (Expr (Ebinop Osub
                               (Expr (Evar (ident_of_nat 1))
                                 (Tint I32 Signed  ))
                               (Expr (Econst_int I32 (repr ? 1))
                                 (Tint I32 Signed  ))) (Tint I32 Signed  )))
                           (Ssequence
                           (Sassign (Expr (Evar (ident_of_nat 1))
                                      (Tint I32 Signed  ))
                             (Expr (Evar (ident_of_nat 2))
                               (Tint I32 Signed  )))
                           (Sifthenelse (Expr (Ebinop Ogt
                                          (Expr (Evar (ident_of_nat 2))
                                            (Tint I32 Signed  ))
                                          (Expr (Econst_int I32 (repr ? 0))
                                            (Tint I32 Signed  )))
                                          (Tint I32 Signed  ))
                             (Sgoto (ident_of_nat 22))
                             Sskip))))))))
                           (LSdefault
                             Sskip)))))))))
         )))
       
       
       
     )〉;
    〈ident_of_nat 23 (* main *), CL_Internal (
      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 24, (Tarray Any (Tint I16 Signed  ) 3)〉 ; 〈ident_of_nat 25, (Tarray Any (Tint I16 Signed  ) 3)〉 ]
        (Ssequence
        (Sassign (Expr (Ederef
                   (Expr (Ebinop Oadd
                     (Expr (Evar (ident_of_nat 24))
                       (Tarray Any (Tint I16 Signed  ) 3))
                     (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
                     (Tpointer Any (Tint I16 Signed  ))))
                   (Tint I16 Signed  ))
          (Expr (Ecast (Tint I16 Signed  )
            (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
            (Tint I16 Signed  )))
        (Ssequence
        (Sassign (Expr (Ederef
                   (Expr (Ebinop Oadd
                     (Expr (Evar (ident_of_nat 24))
                       (Tarray Any (Tint I16 Signed  ) 3))
                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
                     (Tpointer Any (Tint I16 Signed  ))))
                   (Tint I16 Signed  ))
          (Expr (Ecast (Tint I16 Signed  )
            (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
            (Tint I16 Signed  )))
        (Ssequence
        (Sassign (Expr (Ederef
                   (Expr (Ebinop Oadd
                     (Expr (Evar (ident_of_nat 24))
                       (Tarray Any (Tint I16 Signed  ) 3))
                     (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
                     (Tpointer Any (Tint I16 Signed  ))))
                   (Tint I16 Signed  ))
          (Expr (Ecast (Tint I16 Signed  )
            (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
            (Tint I16 Signed  )))
        (Ssequence
        (Scall (None expr) (Expr (Evar (ident_of_nat 0))
                             (Tfunction (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tint I32 Signed  ) Tnil))) Tvoid)) 
          [(Expr (Evar (ident_of_nat 25)) (Tarray Any (Tint I16 Signed  ) 3));
          (Expr (Evar (ident_of_nat 24)) (Tarray Any (Tint I16 Signed  ) 3));
          (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  ))])
        (Sreturn (Some expr (Expr (Ebinop Oadd
                              (Expr (Ebinop Oadd
                                (Expr (Ecast (Tint I32 Signed  )
                                  (Expr (Ederef
                                    (Expr (Ebinop Oadd
                                      (Expr (Evar (ident_of_nat 25))
                                        (Tarray Any (Tint I16 Signed  ) 3))
                                      (Expr (Econst_int I32 (repr ? 0))
                                        (Tint I32 Signed  )))
                                      (Tpointer Any (Tint I16 Signed  ))))
                                    (Tint I16 Signed  )))
                                  (Tint I32 Signed  ))
                                (Expr (Ecast (Tint I32 Signed  )
                                  (Expr (Ederef
                                    (Expr (Ebinop Oadd
                                      (Expr (Evar (ident_of_nat 25))
                                        (Tarray Any (Tint I16 Signed  ) 3))
                                      (Expr (Econst_int I32 (repr ? 1))
                                        (Tint I32 Signed  )))
                                      (Tpointer Any (Tint I16 Signed  ))))
                                    (Tint I16 Signed  )))
                                  (Tint I32 Signed  ))) (Tint I32 Signed  ))
                              (Expr (Ecast (Tint I32 Signed  )
                                (Expr (Ederef
                                  (Expr (Ebinop Oadd
                                    (Expr (Evar (ident_of_nat 25))
                                      (Tarray Any (Tint I16 Signed  ) 3))
                                    (Expr (Econst_int I32 (repr ? 2))
                                      (Tint I32 Signed  )))
                                    (Tpointer Any (Tint I16 Signed  ))))
                                  (Tint I16 Signed  ))) (Tint I32 Signed  )))
                              (Tint I32 Signed  ))))))))
      
      
      
    )〉]
  (ident_of_nat 23)
  
.

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