source: src/Cminor/test/sum-bad.ma @ 762

Last change on this file since 762 was 761, checked in by campbell, 10 years ago

Enforce the use of declared identifiers/registers in Cminor/RTLabs.

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