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

Last change on this file since 2391 was 2391, checked in by campbell, 7 years ago

Revert "Put the post-loop cost label into the Clight while statement ..."
Rely on the Cminor to RTLabs stage ignoring Cminor skips instead.
This reverts commit 2353.
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         (Ssequence
32         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
33           (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
34         (Ssequence
35         (Sfor (Sassign (Expr (Evar (ident_of_nat 5)) (Tint I32 Signed  ))
36                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
37           (Expr (Evar (ident_of_nat 5)) (Tint I32 Signed  ))
38           (Ssequence
39           (Ssequence
40           (Sassign (Expr (Evar (ident_of_nat 6)) (Tint I32 Signed  ))
41             (Expr (Ebinop Osub
42               (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
43               (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
44               (Tint I32 Signed  )))
45           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
46             (Expr (Evar (ident_of_nat 6)) (Tint I32 Signed  ))))
47           (Sassign (Expr (Evar (ident_of_nat 5)) (Tint I32 Signed  ))
48             (Expr (Evar (ident_of_nat 6)) (Tint I32 Signed  ))))
49           (Sifthenelse (Expr (Ebinop Omod
50                          (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
51                          (Expr (Econst_int I32 (repr ? 2))
52                            (Tint I32 Signed  ))) (Tint I32 Signed  ))
53             (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
54               (Expr (Ebinop Oadd
55                 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
56                 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
57                 (Tint I32 Signed  )))
58             (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
59               (Expr (Ebinop Oadd
60                 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
61                 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
62                 (Tint I32 Signed  ))))
63         )
64         (Ssequence
65         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
66           (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
67         (Ssequence
68         (Sdowhile (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
69           (Ssequence
70           (Sifthenelse (Expr (Ebinop Omod
71                          (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
72                          (Expr (Econst_int I32 (repr ? 2))
73                            (Tint I32 Signed  ))) (Tint I32 Signed  ))
74             (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
75               (Expr (Ebinop Oadd
76                 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
77                 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
78                 (Tint I32 Signed  )))
79             (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
80               (Expr (Ebinop Oadd
81                 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
82                 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
83                 (Tint I32 Signed  ))))
84           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
85             (Expr (Ebinop Osub
86               (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
87               (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
88               (Tint I32 Signed  )))))
89         (Ssequence
90         (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
91                 (Expr (Econst_int I32 (repr ? 7)) (Tint I32 Signed  )))
92           (Expr (Ebinop Ogt
93             (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
94             (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
95             (Tint I32 Signed  ))
96           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
97             (Expr (Ebinop Osub
98               (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
99               (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
100               (Tint I32 Signed  )))
101           (Ssequence
102           (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
103             (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
104           (Swhile (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  ))
105             (Ssequence
106             (Ssequence
107             (Ssequence
108             (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
109               (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
110             (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
111               (Expr (Ebinop Osub
112                 (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
113                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
114                 (Tint I32 Signed  ))))
115             (Sifthenelse (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
116               Sskip
117               Sbreak))
118             (Ssequence
119             (Sifthenelse (Expr (Ebinop Olt
120                            (Expr (Evar (ident_of_nat 2))
121                              (Tint I32 Signed  ))
122                            (Expr (Ebinop Odiv
123                              (Expr (Evar (ident_of_nat 1))
124                                (Tint I32 Signed  ))
125                              (Expr (Econst_int I32 (repr ? 2))
126                                (Tint I32 Signed  ))) (Tint I32 Signed  )))
127                            (Tint I32 Signed  ))
128               Sbreak
129               Sskip)
130             (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
131               (Expr (Ebinop Oadd
132                 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
133                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
134                 (Tint I32 Signed  )))))))
135         )
136         (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
137                               (Tint I32 Signed  ))))))))))))
138       
139       
140       
141     )〉]
142  (ident_of_nat 0)
143 
144.
145
146(*
147example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
148normalize  (* you can examine the result here *)
149*)
Note: See TracBrowser for help on using the repository browser.