source: src/Cminor/test/sum.ma @ 758

Last change on this file since 758 was 758, checked in by campbell, 9 years ago

Implement replacement of global var initialisation data by code in Cminor.

File size: 2.2 KB
Line 
1include "Cminor/semantics.ma".
2include "common/Animation.ma".
3
4definition id_src := ident_of_nat 7.
5
6
7definition id_main := ident_of_nat 0.
8definition id_main_tmp0 := ident_of_nat 4.
9definition id_main_total := ident_of_nat 5.
10definition id_main_i := ident_of_nat 6.
11definition C_cost2 := costlabel_of_nat 3.
12definition C_cost0 := costlabel_of_nat 2.
13definition C_cost1 := costlabel_of_nat 1.
14definition f_main := Internal ? (mk_internal_function
15  (mk_signature [] (Some ? ASTint))
16  []
17  [id_main_tmp0; id_main_total; id_main_i]
18  []
19  0 (
20  St_cost C_cost2 (
21  St_seq (
22    St_assign id_main_total (Cst (Ointconst (repr 0)))
23  ) (
24  St_seq (
25    St_seq (
26      St_seq (
27        St_assign id_main_i (Cst (Ointconst (repr 0)))
28      ) (
29      St_block (
30        St_loop (
31          St_seq (
32            St_ifthenelse (Op1 Onotbool (Op2 (Ocmpu Clt) (Id id_main_i) (Cst (Ointconst (repr 5))))) (
33              St_exit 0
34            ) (
35              St_skip            )
36          ) (
37          St_seq (
38            St_block (
39              St_cost C_cost0 (
40              St_assign id_main_total (Op2 Oadd (Op1 Ocast8unsigned (Id id_main_total)) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Cst (Oaddrsymbol id_src (repr 0))) (Op2 Omul (Id id_main_i) (Cst (Ointconst (repr 1))))))))
41              )
42            )
43          ) (
44          St_assign id_main_i (Op2 Oadd (Id id_main_i) (Cst (Ointconst (repr 1))))
45          )
46          )
47        )
48      )
49      )
50    ) (
51    St_cost C_cost1 (
52    St_skip    )
53    )
54  ) (
55  St_return (Some ? (Op1 Ocast8unsigned (Id id_main_total)))
56  )
57  )
58  )
59
60)).
61
62
63
64definition myprog : Cminor_program :=
65mk_program ?? [
66  (pair ?? id_main f_main)
67]  id_main
68[(pair ?? (pair ?? (pair ?? id_src [Init_int8 (repr 28);Init_int8 (repr 17);Init_int8 (repr 17);Init_int8 (repr 8);Init_int8 (repr 4)]) Any) it)]
69.
70
71example exec: finishes_with (repr 74) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
72normalize  (* you can examine the result here *)
73@refl
74qed.
75
76include "Cminor/initialisation.ma".
77
78example exec2: finishes_with (repr 74) ? (exec_up_to Cminor_fullexec (replace_init myprog) 1000 [ ]).
79normalize in ⊢ (???(??%??)) (* examine the program here *)
80normalize  (* you can examine the result here *)
81@refl
82qed.
Note: See TracBrowser for help on using the repository browser.