source: src/Cminor/test/search.Cminor.ma @ 1633

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

Update Cminor pretty printer and examples.
File size: 17.3 KB
Line 
1include "Cminor/semantics.ma".
2include "common/Animation.ma".
3
4definition label_of_nat : nat -> identifier Label := identifier_of_nat ?.
5
6
7
8definition id__div32u := ident_of_nat 0.
9definition id__div32u_quo := ident_of_nat 6.
10definition id__div32u_rem := ident_of_nat 7.
11definition id__div32u_x := ident_of_nat 8.
12definition id__div32u_y := ident_of_nat 9.
13definition C_cost2 := costlabel_of_nat 5.
14definition L_tmp_0 := label_of_nat 4.
15definition C_cost0 := costlabel_of_nat 3.
16definition L_tmp_1 := label_of_nat 2.
17definition C_cost1 := costlabel_of_nat 1.
18definition f__div32u := Internal ? (mk_internal_function
19  (Some ? (ASTint I32 Unsigned))
20  [mk_Prod ?? id__div32u_x (ASTint I32 Unsigned); mk_Prod ?? id__div32u_y (ASTint I32 Unsigned)]
21  [mk_Prod ?? id__div32u_quo (ASTint I32 Unsigned); mk_Prod ?? id__div32u_rem (ASTint I32 Unsigned)]
22  (match daemon in False with [ ])
230 (
24  St_cost C_cost2 (
25  St_seq (
26    St_assign (ASTint I32 Unsigned) id__div32u_quo (Op1 (ASTint I8 Signed) (ASTint I32 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
27  ) (
28  St_seq (
29    St_assign (ASTint I32 Unsigned) id__div32u_rem (Id (ASTint I32 Unsigned) id__div32u_x)
30  ) (
31  St_seq (
32    St_seq (
33      St_seq (
34        St_label L_tmp_0 (
35        St_seq (
36          St_ifthenelse I32 Signed (Op2 (ASTint I32 Unsigned) (ASTint I32 Unsigned) (ASTint I32 Signed) (Ocmpu Cge) (Id (ASTint I32 Unsigned) id__div32u_rem) (Id (ASTint I32 Unsigned) id__div32u_y)) (
37            St_skip          ) (
38            St_goto L_tmp_1
39          )
40        ) (
41        St_seq (
42          St_cost C_cost0 (
43          St_seq (
44            St_assign (ASTint I32 Unsigned) id__div32u_rem (Op2 (ASTint I32 Unsigned) (ASTint I32 Unsigned) (ASTint I32 Unsigned) Osub (Id (ASTint I32 Unsigned) id__div32u_rem) (Id (ASTint I32 Unsigned) id__div32u_y))
45          ) (
46          St_assign (ASTint I32 Unsigned) id__div32u_quo (Op2 (ASTint I32 Unsigned) (ASTint I32 Unsigned) (ASTint I32 Unsigned) Oadd (Id (ASTint I32 Unsigned) id__div32u_quo) (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint ????) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
47          )
48          )
49        ) (
50        St_goto L_tmp_0
51        )
52        )
53        )
54      ) (
55      St_label L_tmp_1 (
56      St_skip      )
57      )
58    ) (
59    St_cost C_cost1 (
60    St_skip    )
61    )
62  ) (
63  St_return (Some ? (mk_DPair ?? (ASTint I32 Unsigned) (Id (ASTint I32 Unsigned) id__div32u_quo)))
64  )
65  )
66  )
67  )
68
69) (match daemon in False with [ ])).
70
71definition id__div32s := ident_of_nat 10.
72definition id__div32s__tmp2 := ident_of_nat 16.
73definition id__div32s_sign := ident_of_nat 17.
74definition id__div32s_x1 := ident_of_nat 18.
75definition id__div32s_y1 := ident_of_nat 19.
76definition id__div32s__tmp_2 := ident_of_nat 20.
77definition id__div32s_x := ident_of_nat 21.
78definition id__div32s_y := ident_of_nat 22.
79definition C_cost7 := costlabel_of_nat 15.
80definition C_cost5 := costlabel_of_nat 14.
81definition C_cost6 := costlabel_of_nat 13.
82definition C_cost3 := costlabel_of_nat 12.
83definition C_cost4 := costlabel_of_nat 11.
84definition f__div32s := Internal ? (mk_internal_function
85  (Some ? (ASTint I32 Signed))
86  [mk_Prod ?? id__div32s_x (ASTint I32 Signed); mk_Prod ?? id__div32s_y (ASTint I32 Signed)]
87  [mk_Prod ?? id__div32s__tmp2 (ASTint I32 Unsigned); mk_Prod ?? id__div32s_sign (ASTint I32 Signed); mk_Prod ?? id__div32s_x1 (ASTint I32 Unsigned); mk_Prod ?? id__div32s_y1 (ASTint I32 Unsigned); mk_Prod ?? id__div32s__tmp_2 (ASTint I32 Unsigned)]
88  (match daemon in False with [ ])
890 (
90  St_cost C_cost7 (
91  St_seq (
92    St_assign (ASTint I32 Unsigned) id__div32s_x1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint ????) (Id (ASTint I32 Signed) id__div32s_x))
93  ) (
94  St_seq (
95    St_assign (ASTint I32 Unsigned) id__div32s_y1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint ????) (Id (ASTint I32 Signed) id__div32s_y))
96  ) (
97  St_seq (
98    St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))
99  ) (
100  St_seq (
101    St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Clt) (Id (ASTint I32 Signed) id__div32s_x) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))) (
102      St_cost C_cost5 (
103      St_seq (
104        St_assign (ASTint I32 Unsigned) id__div32s_x1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint ????) (Op1 (ASTint I32 Signed) (ASTint I32 Signed) (Onegint ??) (Id (ASTint I32 Signed) id__div32s_x)))
105      ) (
106      St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I32 Signed) (ASTint I32 Signed) (Onegint ??) (Id (ASTint I32 Signed) id__div32s_sign))
107      )
108      )
109    ) (
110      St_cost C_cost6 (
111      St_skip      )
112    )
113  ) (
114  St_seq (
115    St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Clt) (Id (ASTint I32 Signed) id__div32s_y) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))) (
116      St_cost C_cost3 (
117      St_seq (
118        St_assign (ASTint I32 Unsigned) id__div32s_y1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint ????) (Op1 (ASTint I32 Signed) (ASTint I32 Signed) (Onegint ??) (Id (ASTint I32 Signed) id__div32s_y)))
119      ) (
120      St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I32 Signed) (ASTint I32 Signed) (Onegint ??) (Id (ASTint I32 Signed) id__div32s_sign))
121      )
122      )
123    ) (
124      St_cost C_cost4 (
125      St_skip      )
126    )
127  ) (
128  St_seq (
129    St_seq (
130      St_call (Some ? (mk_Prod ?? id__div32s__tmp_2 (ASTint I32 Unsigned))) (Cst ? (Oaddrsymbol id__div32u 0)) [mk_DPair ?? (ASTint I32 Unsigned) (Id (ASTint I32 Unsigned) id__div32s_x1); mk_DPair ?? (ASTint I32 Unsigned) (Id (ASTint I32 Unsigned) id__div32s_y1)]
131    ) (
132    St_assign (ASTint I32 Unsigned) id__div32s__tmp2 (Id (ASTint I32 Unsigned) id__div32s__tmp_2)
133    )
134  ) (
135  St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Id (ASTint I32 Signed) id__div32s_sign) (Op1 (ASTint I32 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I32 Unsigned) id__div32s__tmp2)))))
136  )
137  )
138  )
139  )
140  )
141  )
142  )
143
144) (match daemon in False with [ ])).
145
146definition id_search := ident_of_nat 23.
147definition id_search__tmp4 := ident_of_nat 35.
148definition id_search_high := ident_of_nat 36.
149definition id_search_i := ident_of_nat 37.
150definition id_search_low := ident_of_nat 38.
151definition id_search__tmp_5 := ident_of_nat 39.
152definition id_search_tab := ident_of_nat 40.
153definition id_search_size := ident_of_nat 41.
154definition id_search_to_find := ident_of_nat 42.
155definition C_cost16 := costlabel_of_nat 34.
156definition L_tmp_3 := label_of_nat 33.
157definition C_cost14 := costlabel_of_nat 32.
158definition C_cost12 := costlabel_of_nat 31.
159definition C_cost13 := costlabel_of_nat 30.
160definition C_cost10 := costlabel_of_nat 29.
161definition C_cost11 := costlabel_of_nat 28.
162definition C_cost8 := costlabel_of_nat 27.
163definition C_cost9 := costlabel_of_nat 26.
164definition L_tmp_4 := label_of_nat 25.
165definition C_cost15 := costlabel_of_nat 24.
166definition f_search := Internal ? (mk_internal_function
167  (Some ? (ASTint I8 Unsigned))
168  [mk_Prod ?? id_search_tab (ASTptr Any); mk_Prod ?? id_search_size (ASTint I8 Unsigned); mk_Prod ?? id_search_to_find (ASTint I8 Unsigned)]
169  [mk_Prod ?? id_search__tmp4 (ASTint I32 Signed); mk_Prod ?? id_search_high (ASTint I8 Unsigned); mk_Prod ?? id_search_i (ASTint I8 Unsigned); mk_Prod ?? id_search_low (ASTint I8 Unsigned); mk_Prod ?? id_search__tmp_5 (ASTint I32 Signed)]
170  (match daemon in False with [ ])
1710 (
172  St_cost C_cost16 (
173  St_seq (
174    St_assign (ASTint I8 Unsigned) id_search_low (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
175  ) (
176  St_seq (
177    St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Osub (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_size)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
178  ) (
179  St_seq (
180    St_seq (
181      St_seq (
182        St_label L_tmp_3 (
183        St_seq (
184          St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cge) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_high)) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_low))) (
185            St_skip          ) (
186            St_goto L_tmp_4
187          )
188        ) (
189        St_seq (
190          St_cost C_cost14 (
191          St_seq (
192            St_seq (
193              St_call (Some ? (mk_Prod ?? id_search__tmp_5 (ASTint I32 Signed))) (Cst ? (Oaddrsymbol id__div32s 0)) [mk_DPair ?? (ASTint I32 Signed) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Oadd (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_high)) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_low))); mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 2))))]
194            ) (
195            St_assign (ASTint I32 Signed) id_search__tmp4 (Id (ASTint I32 Signed) id_search__tmp_5)
196            )
197          ) (
198          St_seq (
199            St_assign (ASTint I8 Unsigned) id_search_i (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Id (ASTint I32 Signed) id_search__tmp4))
200          ) (
201          St_seq (
202            St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Ceq) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1))))))) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_to_find))) (
203              St_cost C_cost12 (
204              St_return (Some ? (mk_DPair ?? (ASTint I8 Unsigned) (Id (ASTint I8 Unsigned) id_search_i)))
205              )
206            ) (
207              St_cost C_cost13 (
208              St_skip              )
209            )
210          ) (
211          St_seq (
212            St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cgt) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1))))))) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_to_find))) (
213              St_cost C_cost10 (
214              St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Osub (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_i)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
215              )
216            ) (
217              St_cost C_cost11 (
218              St_skip              )
219            )
220          ) (
221          St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Clt) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1))))))) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_to_find))) (
222            St_cost C_cost8 (
223            St_assign (ASTint I8 Unsigned) id_search_low (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Oadd (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_i)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
224            )
225          ) (
226            St_cost C_cost9 (
227            St_skip            )
228          )
229          )
230          )
231          )
232          )
233          )
234        ) (
235        St_goto L_tmp_3
236        )
237        )
238        )
239      ) (
240      St_label L_tmp_4 (
241      St_skip      )
242      )
243    ) (
244    St_cost C_cost15 (
245    St_skip    )
246    )
247  ) (
248  St_return (Some ? (mk_DPair ?? (ASTint I8 Unsigned) (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Op1 (ASTint I32 Signed) (ASTint I32 Signed) (Onegint ??) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))))
249  )
250  )
251  )
252  )
253
254) (match daemon in False with [ ])).
255
256definition id_main := ident_of_nat 43.
257definition id_main_res := ident_of_nat 45.
258definition id_main__tmp_6 := ident_of_nat 46.
259definition C_cost17 := costlabel_of_nat 44.
260definition f_main := Internal ? (mk_internal_function
261  (Some ? (ASTint I32 Signed))
262  []
263  [mk_Prod ?? id_main_res (ASTint I8 Unsigned); mk_Prod ?? id_main__tmp_6 (ASTint I8 Unsigned)]
264  (match daemon in False with [ ])
2655 (
266  St_cost C_cost17 (
267  St_seq (
268    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
269  ) (
270  St_seq (
271    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 18))))
272  ) (
273  St_seq (
274    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 2))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 23))))
275  ) (
276  St_seq (
277    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 3))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 57))))
278  ) (
279  St_seq (
280    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 4))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 120))))
281  ) (
282  St_seq (
283    St_seq (
284      St_call (Some ? (mk_Prod ?? id_main__tmp_6 (ASTint I8 Unsigned))) (Cst ? (Oaddrsymbol id_search 0)) [mk_DPair ?? (ASTptr Any) (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))); mk_DPair ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 5)))); mk_DPair ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 57))))]
285    ) (
286    St_assign (ASTint I8 Unsigned) id_main_res (Id (ASTint I8 Unsigned) id_main__tmp_6)
287    )
288  ) (
289  St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_main_res))))
290  )
291  )
292  )
293  )
294  )
295  )
296  )
297
298) (match daemon in False with [ ])).
299
300
301
302definition myprog : Cminor_program :=
303mk_program ?? [] [
304  (mk_Prod ?? id__div32u f__div32u);
305  (mk_Prod ?? id__div32s f__div32s);
306  (mk_Prod ?? id_search f_search);
307  (mk_Prod ?? id_main f_main)
308]  id_main
309.
Note: See TracBrowser for help on using the repository browser.