source: Deliverables/D3.3/id-lookup-branch/Cminor/test/search.Cminor.ma @ 2113

Last change on this file since 2113 was 1311, checked in by campbell, 10 years ago

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