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

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

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

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 ??.
75[normalize  (* you can examine the result here *)
76 @refl
77|skip
78]
79qed.
80
81include "Cminor/initialisation.ma".
82
83example exec2: exec_up_to Cminor_fullexec (replace_init myprog) 1000 [ ] = Error ??.
84[normalize  (* you can examine the result here *)
85 @refl
86|skip
87]
88qed.
Note: See TracBrowser for help on using the repository browser.