source: src/Cminor/test/null-op.ma @ 879

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

Refine "AST" types to include size/signedness information.

File size: 2.5 KB
Line 
1include "Cminor/semantics.ma".
2include "common/Animation.ma".
3
4(* NB: I've had to add Optrofint in a couple of places because the prototype
5       isn't handling conversions between zero and null pointers at the moment.
6       *)
7
8definition id_main := ident_of_nat 0.
9definition id_main_tmp0 := ident_of_nat 6.
10definition id_main_q := ident_of_nat 7.
11definition id_main_p := ident_of_nat 8.
12definition id_main_c := ident_of_nat 9.
13definition C_cost4 := costlabel_of_nat 5.
14definition C_cost2 := costlabel_of_nat 4.
15definition C_cost3 := costlabel_of_nat 3.
16definition C_cost0 := costlabel_of_nat 2.
17definition C_cost1 := costlabel_of_nat 1.
18definition f_main := Internal ? (mk_internal_function
19  (mk_signature [] (Some ? (ASTint I32 Signed)))
20  []
21  [id_main_tmp0; id_main_q; id_main_p; id_main_c]
22  [id_main_q; id_main_p]
23  1 (
24  St_cost C_cost4 (
25  St_seq (
26    St_assign id_main_p (Op1 (Optrofint Any) (Cst (Ointconst (repr 0))))
27  ) (
28  St_seq (
29    St_assign id_main_q (Cst (Oaddrstack (repr 0)))
30  ) (
31  St_seq (
32    St_ifthenelse (Op2 (Ocmpp Ceq) (Id id_main_p) (Id id_main_q)) (
33      St_cost C_cost2 (
34      St_return (Some ? (Cst (Ointconst (repr 0))))
35      )
36    ) (
37      St_cost C_cost3 (
38      St_skip      )
39    )
40  ) (
41  St_seq (
42    St_ifthenelse (Op2 (Ocmp Cgt) (Op2 Osubpp (Id id_main_p) (Id id_main_p)) (Cst (Ointconst (repr 0)))) (
43      St_cost C_cost0 (
44      St_return (Some ? (Cst (Ointconst (repr 0))))
45      )
46    ) (
47      St_cost C_cost1 (
48      St_skip      )
49    )
50  ) (
51  St_seq (
52    St_assign id_main_p (Op2 Oaddp (Id id_main_p) (Op2 Omul (Cst (Ointconst (repr 0))) (Cst (Ointconst (repr 1)))))
53  ) (
54  St_seq (
55    St_assign id_main_p (Op2 Oaddp (Id id_main_p) (Op2 Omul (Cst (Ointconst (repr 0))) (Cst (Ointconst (repr 1)))))
56  ) (
57  St_seq (
58    St_assign id_main_p (Op2 Osubpi (Id id_main_p) (Op2 Omul (Cst (Ointconst (repr 0))) (Cst (Ointconst (repr 1)))))
59  ) (
60  St_return (Some ? (Op2 (Ocmpp Ceq) (Id id_main_p) (Op1 (Optrofint Any) (Cst (Ointconst (repr 0))))))
61  )
62  )
63  )
64  )
65  )
66  )
67  )
68  )
69
70)).
71
72
73
74definition myprog : Cminor_program :=
75mk_program ?? [
76  (pair ?? id_main f_main)
77]  id_main
78[]
79.
80
81example exec: finishes_with (repr 1) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
82normalize  (* you can examine the result here *)
83@refl
84qed.
85
86include "Cminor/toRTLabs.ma".
87include "RTLabs/semantics.ma".
88
89example execRTL: finishes_with (repr 1) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
90normalize  (* you can examine the result here *)
91@refl
92qed.
93
Note: See TracBrowser for help on using the repository browser.