include "Clight/Animation.ma".

definition myprog := mk_program fundef type
  [〈succ_pos_of_nat 0 (* dosomething *), External (succ_pos_of_nat 0) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )〉;
  〈succ_pos_of_nat 1 (* main *), Internal (
    mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 3, (Tint I32 Signed  )〉 ]
      (Ssequence
      (Sassign (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  ))
        (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
      (Ssequence
      (Ssequence
      (Scall (Some expr (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  )))
        (Expr (Evar (succ_pos_of_nat 0))
          (Tfunction (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )))
        [(Expr (Econst_int (repr 10)) (Tint I32 Signed  ))])
      (Sassign (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  ))
        (Expr (Ebinop Oadd
          (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  ))
          (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  )))
          (Tint I32 Signed  ))))
      (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 2))
                            (Tint I32 Signed  ))))))
    
    
    
  )〉]
  (succ_pos_of_nat 1)
  []
.

example exec:
 (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 7)]; do r ← opt_to_res … (is_final s); OK ? 〈t,r〉) =
 OK ? 〈[EVextcall (succ_pos_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 9〉.
normalize  (* you can examine the result here *)
@refl
qed.