source: src/Clight/test/switcher.ma @ 779

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

Clight and Cminor examples for switch statement.

File size: 4.0 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program clight_fundef type
5  [〈ident_of_nat 0 (* get *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
6  〈ident_of_nat 1 (* main *), CL_Internal (
7    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ]
8      (Ssequence
9      (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
10        (Expr (Ecast (Tint I8 Unsigned )
11          (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
12          (Tint I8 Unsigned )))
13      (Ssequence
14      (Ssequence
15      (Scall (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))
16        (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed  )))
17        [])
18      (Sswitch (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )) (
19        (LScase (repr 1)
20          Sbreak
21          (LScase (repr 3)
22            (Ssequence
23            (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
24              (Expr (Ecast (Tint I8 Unsigned )
25                (Expr (Ebinop Oadd
26                  (Expr (Ecast (Tint I32 Signed  )
27                    (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
28                    (Tint I32 Signed  ))
29                  (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
30                  (Tint I32 Signed  ))) (Tint I8 Unsigned )))
31            Sbreak)
32            (LScase (repr 5)
33              (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
34                (Expr (Ecast (Tint I8 Unsigned )
35                  (Expr (Ebinop Oadd
36                    (Expr (Ecast (Tint I32 Signed  )
37                      (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
38                      (Tint I32 Signed  ))
39                    (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
40                    (Tint I32 Signed  ))) (Tint I8 Unsigned )))
41              (LScase (repr 7)
42                (Ssequence
43                (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
44                  (Expr (Ecast (Tint I8 Unsigned )
45                    (Expr (Ebinop Oadd
46                      (Expr (Ecast (Tint I32 Signed  )
47                        (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
48                        (Tint I32 Signed  ))
49                      (Expr (Econst_int (repr 3)) (Tint I32 Signed  )))
50                      (Tint I32 Signed  ))) (Tint I8 Unsigned )))
51                Sbreak)
52                (LSdefault
53                  (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
54                    (Expr (Ecast (Tint I8 Unsigned )
55                      (Expr (Ebinop Oadd
56                        (Expr (Ecast (Tint I32 Signed  )
57                          (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
58                          (Tint I32 Signed  ))
59                        (Expr (Econst_int (repr 16)) (Tint I32 Signed  )))
60                        (Tint I32 Signed  ))) (Tint I8 Unsigned ))))))))
61      )))
62      (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
63                            (Expr (Evar (ident_of_nat 2))
64                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))
65   
66   
67   
68  )〉]
69  (ident_of_nat 1)
70  []
71.
72
73example exec0: finishes_with (repr 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 0)]).
74normalize  (* you can examine the result here *)
75@refl qed.
76
77example exec1: finishes_with (repr 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 1)]).
78normalize  (* you can examine the result here *)
79@refl qed.
80
81example exec3: finishes_with (repr 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 3)]).
82normalize  (* you can examine the result here *)
83@refl qed.
84
85example exec5: finishes_with (repr 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 5)]).
86normalize  (* you can examine the result here *)
87@refl qed.
88
89example exec7: finishes_with (repr 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)]).
90normalize  (* you can examine the result here *)
91@refl qed.
Note: See TracBrowser for help on using the repository browser.