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

Last change on this file was 1513, checked in by campbell, 8 years ago

Fix up Clight examples.

File size: 3.6 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × 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))
50                          (Tint I32 Signed  ))) (Tint I32 Signed  )))
51                      (Tint I8 Unsigned )))
52                  Sbreak)
53                  (LSdefault
54                    (Sassign (Expr (Evar (ident_of_nat 2))
55                               (Tint I8 Unsigned ))
56                      (Expr (Ecast (Tint I8 Unsigned )
57                        (Expr (Ebinop Oadd
58                          (Expr (Ecast (Tint I32 Signed  )
59                            (Expr (Evar (ident_of_nat 2))
60                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))
61                          (Expr (Econst_int I32 (repr ? 16))
62                            (Tint I32 Signed  ))) (Tint I32 Signed  )))
63                        (Tint I8 Unsigned ))))))))
64        )))
65        (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
66                              (Expr (Evar (ident_of_nat 2))
67                                (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))
68     
69     
70     
71    )〉]
72  (ident_of_nat 1)
73 
74.
75
76(*
77example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
78normalize  (* you can examine the result here *)
79*)
Note: See TracBrowser for help on using the repository browser.