source: src/Clight/test/switcher.c.ma @ 978

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

Update remaining Clight examples.

File size: 4.1 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 I32 (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 I32 (repr ? 1)
20          Sbreak
21          (LScase I32 (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 I32 (repr ? 1)) (Tint I32 Signed  )))
30                  (Tint I32 Signed  ))) (Tint I8 Unsigned )))
31            Sbreak)
32            (LScase I32 (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 I32 (repr ? 2)) (Tint I32 Signed  )))
40                    (Tint I32 Signed  ))) (Tint I8 Unsigned )))
41              (LScase I32 (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 I32 (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 I32 (repr ? 16))
60                          (Tint I32 Signed  ))) (Tint I32 Signed  )))
61                      (Tint I8 Unsigned ))))))))
62      )))
63      (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
64                            (Expr (Evar (ident_of_nat 2))
65                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))
66   
67   
68   
69  )〉]
70  (ident_of_nat 1)
71  []
72.
73
74example exec0: finishes_with (repr I32 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 0)]).
75normalize  (* you can examine the result here *)
76@refl qed.
77
78example exec1: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 1)]).
79normalize  (* you can examine the result here *)
80@refl qed.
81
82example exec3: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 3)]).
83normalize  (* you can examine the result here *)
84@refl qed.
85
86example exec5: finishes_with (repr I32 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
87normalize  (* you can examine the result here *)
88@refl qed.
89
90example exec7: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 7)]).
91normalize  (* you can examine the result here *)
92@refl qed.
Note: See TracBrowser for help on using the repository browser.