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

Last change on this file since 1680 was 1633, checked in by campbell, 8 years ago

Update Cminor pretty printer and examples.

File size: 3.3 KB
Line 
1include "Cminor/semantics.ma".
2include "common/Animation.ma".
3
4definition label_of_nat : nat -> identifier Label := identifier_of_nat ?.
5
6
7
8definition id_main := ident_of_nat 0.
9definition id_main_p := ident_of_nat 6.
10definition id_main_q := ident_of_nat 7.
11definition C_cost4 := costlabel_of_nat 5.
12definition C_cost2 := costlabel_of_nat 4.
13definition C_cost3 := costlabel_of_nat 3.
14definition C_cost0 := costlabel_of_nat 2.
15definition C_cost1 := costlabel_of_nat 1.
16definition f_main := Internal ? (mk_internal_function
17  (Some ? (ASTint I32 Signed))
18  []
19  [mk_Prod ?? id_main_p (ASTptr Any); mk_Prod ?? id_main_q (ASTptr Any)]
20  (match daemon in False with [ ])
211 (
22  St_cost C_cost4 (
23  St_seq (
24    St_assign (ASTptr Any) id_main_p (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint ?? Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
25  ) (
26  St_seq (
27    St_assign (ASTptr Any) id_main_q (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0))))
28  ) (
29  St_seq (
30    St_ifthenelse I32 Signed (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Id (ASTptr Any) id_main_q)) (
31      St_cost C_cost2 (
32      St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
33      )
34    ) (
35      St_cost C_cost3 (
36      St_skip      )
37    )
38  ) (
39  St_seq (
40    St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cgt) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Osubpp I32) (Id (ASTptr Any) id_main_p) (Id (ASTptr Any) id_main_p)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))) (
41      St_cost C_cost0 (
42      St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
43      )
44    ) (
45      St_cost C_cost1 (
46      St_skip      )
47    )
48  ) (
49  St_seq (
50    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
51  ) (
52  St_seq (
53    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
54  ) (
55  St_seq (
56    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Osubpi (Id (ASTptr Any) id_main_p) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
57  ) (
58  St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Op1 (ASTint I32 Signed) (ASTptr Any) (Optrofint ?? Any) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))))))
59  )
60  )
61  )
62  )
63  )
64  )
65  )
66  )
67
68) (match daemon in False with [ ])).
69
70
71
72definition myprog : Cminor_program :=
73mk_program ?? [] [
74  (mk_Prod ?? id_main f_main)
75]  id_main
76.
Note: See TracBrowser for help on using the repository browser.