source: src/Clight/test/controlflow.c.ma @ 2388

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

Example of each type of control flow statement, plus minor fix to matita
pretty printer.

File size: 7.5 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 (* main *), CL_Internal (
6       mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ; 〈ident_of_nat 4, (Tint I32 Signed  )〉 ; 〈ident_of_nat 5, (Tint I32 Signed  )〉 ; 〈ident_of_nat 6, (Tint I32 Signed  )〉 ]
7         (Ssequence
8         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
9           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
10         (Ssequence
11         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
12           (Expr (Econst_int I32 (repr ? 10)) (Tint I32 Signed  )))
13         (Ssequence
14         (Swhile (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
15           (Ssequence
16           (Sifthenelse (Expr (Ebinop Omod
17                          (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
18                          (Expr (Econst_int I32 (repr ? 2))
19                            (Tint I32 Signed  ))) (Tint I32 Signed  ))
20             (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
21               (Expr (Ebinop Oadd
22                 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
23                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
24                 (Tint I32 Signed  )))
25             Sskip)
26           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
27             (Expr (Ebinop Osub
28               (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
29               (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
30               (Tint I32 Signed  ))))
31         (None ?))
32         (Ssequence
33         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
34           (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
35         (Ssequence
36         (Sfor (Sassign (Expr (Evar (ident_of_nat 5)) (Tint I32 Signed  ))
37                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
38           (Expr (Evar (ident_of_nat 5)) (Tint I32 Signed  ))
39           (Ssequence
40           (Ssequence
41           (Sassign (Expr (Evar (ident_of_nat 6)) (Tint I32 Signed  ))
42             (Expr (Ebinop Osub
43               (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
44               (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
45               (Tint I32 Signed  )))
46           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
47             (Expr (Evar (ident_of_nat 6)) (Tint I32 Signed  ))))
48           (Sassign (Expr (Evar (ident_of_nat 5)) (Tint I32 Signed  ))
49             (Expr (Evar (ident_of_nat 6)) (Tint I32 Signed  ))))
50           (Sifthenelse (Expr (Ebinop Omod
51                          (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
52                          (Expr (Econst_int I32 (repr ? 2))
53                            (Tint I32 Signed  ))) (Tint I32 Signed  ))
54             (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
55               (Expr (Ebinop Oadd
56                 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
57                 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
58                 (Tint I32 Signed  )))
59             (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
60               (Expr (Ebinop Oadd
61                 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
62                 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
63                 (Tint I32 Signed  ))))
64         )
65         (Ssequence
66         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
67           (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
68         (Ssequence
69         (Sdowhile (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
70           (Ssequence
71           (Sifthenelse (Expr (Ebinop Omod
72                          (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
73                          (Expr (Econst_int I32 (repr ? 2))
74                            (Tint I32 Signed  ))) (Tint I32 Signed  ))
75             (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
76               (Expr (Ebinop Oadd
77                 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
78                 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
79                 (Tint I32 Signed  )))
80             (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
81               (Expr (Ebinop Oadd
82                 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
83                 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
84                 (Tint I32 Signed  ))))
85           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
86             (Expr (Ebinop Osub
87               (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
88               (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
89               (Tint I32 Signed  )))))
90         (Ssequence
91         (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
92                 (Expr (Econst_int I32 (repr ? 7)) (Tint I32 Signed  )))
93           (Expr (Ebinop Ogt
94             (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
95             (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
96             (Tint I32 Signed  ))
97           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
98             (Expr (Ebinop Osub
99               (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
100               (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
101               (Tint I32 Signed  )))
102           (Ssequence
103           (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
104             (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
105           (Swhile (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  ))
106             (Ssequence
107             (Ssequence
108             (Ssequence
109             (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
110               (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
111             (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
112               (Expr (Ebinop Osub
113                 (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
114                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
115                 (Tint I32 Signed  ))))
116             (Sifthenelse (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
117               Sskip
118               Sbreak))
119             (Ssequence
120             (Sifthenelse (Expr (Ebinop Olt
121                            (Expr (Evar (ident_of_nat 2))
122                              (Tint I32 Signed  ))
123                            (Expr (Ebinop Odiv
124                              (Expr (Evar (ident_of_nat 1))
125                                (Tint I32 Signed  ))
126                              (Expr (Econst_int I32 (repr ? 2))
127                                (Tint I32 Signed  ))) (Tint I32 Signed  )))
128                            (Tint I32 Signed  ))
129               Sbreak
130               Sskip)
131             (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
132               (Expr (Ebinop Oadd
133                 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
134                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
135                 (Tint I32 Signed  )))))
136             (None ?)))
137         )
138         (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
139                               (Tint I32 Signed  ))))))))))))
140       
141       
142       
143     )〉]
144  (ident_of_nat 0)
145 
146.
147
148(*
149example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
150normalize  (* you can examine the result here *)
151*)
Note: See TracBrowser for help on using the repository browser.