source: src/RTLabs/test/sum.ma @ 1226

include "RTLabs/import.ma".
include "common/Animation.ma".

definition id_src := ident_of_nat 1.



  definition id_main := ident_of_nat 0.
  definition main9 := 30.
  definition main8 := 29.
  definition main7 := 28.
  definition main6 := 27.
  definition main5 := 26.
  definition main4 := 25.
  definition main30 := 24.
  definition main3 := 23.
  definition main29 := 22.
  definition main28 := 21.
  definition main27 := 20.
  definition main26 := 19.
  definition main25 := 18.
  definition main24 := 17.
  definition main23 := 16.
  definition main22 := 15.
  definition main21 := 14.
  definition main20 := 13.
  definition main2 := 12.
  definition main19 := 11.
  definition main18 := 10.
  definition main17 := 9.
  definition main16 := 8.
  definition main15 := 7.
  definition main14 := 6.
  definition main13 := 5.
  definition main12 := 4.
  definition main11 := 3.
  definition main10 := 2.
  definition main1 := 1.
  definition main0 := 0.
  definition C_cost2 := costlabel_of_nat 2.
  definition C_cost1 := costlabel_of_nat 1.
  definition C_cost0 := costlabel_of_nat 0.


  definition pre_main := mk_pre_internal_function
    (mk_signature [] (Some ? (ASTint I32 Signed)))
    (Some ? 3)
    []
    [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18]
    [8; 9]
    0
    [
    (pair ?? main9 (make_St_op2 Oaddp 8 9 10 main8));
    (pair ?? main8 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[8]] 7 main7));
    (pair ?? main7 (make_St_op1 Ocast8unsigned 6 7 main6));
    (pair ?? main6 (make_St_op2 Oadd 1 5 6 main5));
    (pair ?? main5 (make_St_const 4 (Ointconst (repr 1)) main4));
    (pair ?? main4 (make_St_op2 Oadd 2 2 4 main3));
    (pair ?? main30 (make_St_const 18 (Ointconst (repr 28)) main29));
    (pair ?? main3 (make_St_skip main17));
    (pair ?? main29 (make_St_store Mint8unsigned (Aglobal id_src (repr 0)) [[]] 18 main28));
    (pair ?? main28 (make_St_const 17 (Ointconst (repr 17)) main27));
    (pair ?? main27 (make_St_store Mint8unsigned (Aglobal id_src (repr 1)) [[]] 17 main26));
    (pair ?? main26 (make_St_const 16 (Ointconst (repr 17)) main25));
    (pair ?? main25 (make_St_store Mint8unsigned (Aglobal id_src (repr 2)) [[]] 16 main24));
    (pair ?? main24 (make_St_const 15 (Ointconst (repr 8)) main23));
    (pair ?? main23 (make_St_store Mint8unsigned (Aglobal id_src (repr 3)) [[]] 15 main22));
    (pair ?? main22 (make_St_const 14 (Ointconst (repr 4)) main21));
    (pair ?? main21 (make_St_store Mint8unsigned (Aglobal id_src (repr 4)) [[]] 14 main20));
    (pair ?? main20 (make_St_cost C_cost2 main19));
    (pair ?? main2 (make_St_cost C_cost1 main1));
    (pair ?? main19 (make_St_const 1 (Ointconst (repr 0)) main18));
    (pair ?? main18 (make_St_const 2 (Ointconst (repr 0)) main3));
    (pair ?? main17 (make_St_const 13 (Ointconst (repr 5)) main16));
    (pair ?? main16 (make_St_op2 (Ocmpu Clt) 12 2 13 main15));
    (pair ?? main15 (make_St_cond1 Onotbool 12 main2 main14));
    (pair ?? main14 (make_St_cost C_cost0 main13));
    (pair ?? main13 (make_St_op1 Ocast8unsigned 5 1 main12));
    (pair ?? main12 (make_St_const 9 (Oaddrsymbol id_src (repr 0)) main11));
    (pair ?? main11 (make_St_const 11 (Ointconst (repr 1)) main10));
    (pair ?? main10 (make_St_op2 Omul 10 2 11 main9));
    (pair ?? main1 (make_St_op1 Ocast8unsigned 3 1 main0));
    (pair ?? main0 (make_St_return))
]

    main30
    main0.



definition prog : res RTLabs_program :=
  do f_main \larr make_internal_function pre_main;

OK ? (mk_program ??
(  (pair ?? id_main f_main)::
(nil ?))
  id_main
  (*globals:*)
  [pair ?? (pair ?? (pair ?? id_src [Init_space 8 ]) Any) it]
).

example exec: finishes_with (repr 74) ? (do myprog ← prog; exec_up_to RTLabs_fullexec myprog 1000 [ ]).
normalize  (* you can examine the result here *)
@refl
qed.