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

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

Fix up some minor null pointer issues in Clight.
Add corresponding Cminor example and fix up pretty printer a little.

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))
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.