Context Navigation

duff.c.ma @ 1513

Last change on this file since 1513 was 1513, checked in by campbell, 9 years ago
Fix up Clight examples.
File size: 23.1 KB

Line
1	include "Clight/Cexec.ma".
2	include "common/Animation.ma".
3
4	definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
5	[][〈ident_of_nat 0 (* copy *), CL_Internal (
6	mk_function Tvoid [〈ident_of_nat 19, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 20, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed )〉 ] [〈ident_of_nat 1, (Tint I32 Signed )〉 ; 〈ident_of_nat 2, (Tint I32 Signed )〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 4, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 7, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 8, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 10, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 11, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 12, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 14, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 15, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 17, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 18, (Tpointer Any (Tint I16 Signed ))〉 ]
7	(Ssequence
8	(Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed ))
9	(Expr (Ebinop Odiv
10	(Expr (Ebinop Oadd
11	(Expr (Evar (ident_of_nat 21)) (Tint I32 Signed ))
12	(Expr (Econst_int I32 (repr ? 7)) (Tint I32 Signed )))
13	(Tint I32 Signed ))
14	(Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed )))
15	(Tint I32 Signed )))
16	(Sswitch (Expr (Ebinop Omod
17	(Expr (Evar (ident_of_nat 21)) (Tint I32 Signed ))
18	(Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed )))
19	(Tint I32 Signed )) (
20	(LScase I32 (repr ? 0)
21	(Slabel (ident_of_nat 22)
22	(Ssequence
23	(Ssequence
24	(Sassign (Expr (Evar (ident_of_nat 17))
25	(Tpointer Any (Tint I16 Signed )))
26	(Expr (Evar (ident_of_nat 19))
27	(Tpointer Any (Tint I16 Signed ))))
28	(Sassign (Expr (Evar (ident_of_nat 19))
29	(Tpointer Any (Tint I16 Signed )))
30	(Expr (Ebinop Oadd
31	(Expr (Evar (ident_of_nat 17))
32	(Tpointer Any (Tint I16 Signed )))
33	(Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed )))
34	(Tpointer Any (Tint I16 Signed )))))
35	(Ssequence
36	(Ssequence
37	(Sassign (Expr (Evar (ident_of_nat 18))
38	(Tpointer Any (Tint I16 Signed )))
39	(Expr (Evar (ident_of_nat 20))
40	(Tpointer Any (Tint I16 Signed ))))
41	(Sassign (Expr (Evar (ident_of_nat 20))
42	(Tpointer Any (Tint I16 Signed )))
43	(Expr (Ebinop Oadd
44	(Expr (Evar (ident_of_nat 18))
45	(Tpointer Any (Tint I16 Signed )))
46	(Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed )))
47	(Tpointer Any (Tint I16 Signed )))))
48	(Sassign (Expr (Ederef
49	(Expr (Evar (ident_of_nat 17))
50	(Tpointer Any (Tint I16 Signed ))))
51	(Tint I16 Signed ))
52	(Expr (Ederef
53	(Expr (Evar (ident_of_nat 18))
54	(Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed ))))))
55	(LScase I32 (repr ? 7)
56	(Ssequence
57	(Sassign (Expr (Evar (ident_of_nat 15))
58	(Tpointer Any (Tint I16 Signed )))
59	(Expr (Evar (ident_of_nat 19))
60	(Tpointer Any (Tint I16 Signed ))))
61	(Ssequence
62	(Sassign (Expr (Evar (ident_of_nat 19))
63	(Tpointer Any (Tint I16 Signed )))
64	(Expr (Ebinop Oadd
65	(Expr (Evar (ident_of_nat 15))
66	(Tpointer Any (Tint I16 Signed )))
67	(Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed )))
68	(Tpointer Any (Tint I16 Signed ))))
69	(Ssequence
70	(Sassign (Expr (Evar (ident_of_nat 16))
71	(Tpointer Any (Tint I16 Signed )))
72	(Expr (Evar (ident_of_nat 20))
73	(Tpointer Any (Tint I16 Signed ))))
74	(Ssequence
75	(Sassign (Expr (Evar (ident_of_nat 20))
76	(Tpointer Any (Tint I16 Signed )))
77	(Expr (Ebinop Oadd
78	(Expr (Evar (ident_of_nat 16))
79	(Tpointer Any (Tint I16 Signed )))
80	(Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed )))
81	(Tpointer Any (Tint I16 Signed ))))
82	(Sassign (Expr (Ederef
83	(Expr (Evar (ident_of_nat 15))
84	(Tpointer Any (Tint I16 Signed ))))
85	(Tint I16 Signed ))
86	(Expr (Ederef
87	(Expr (Evar (ident_of_nat 16))
88	(Tpointer Any (Tint I16 Signed ))))
89	(Tint I16 Signed )))))))
90	(LScase I32 (repr ? 6)
91	(Ssequence
92	(Sassign (Expr (Evar (ident_of_nat 13))
93	(Tpointer Any (Tint I16 Signed )))
94	(Expr (Evar (ident_of_nat 19))
95	(Tpointer Any (Tint I16 Signed ))))
96	(Ssequence
97	(Sassign (Expr (Evar (ident_of_nat 19))
98	(Tpointer Any (Tint I16 Signed )))
99	(Expr (Ebinop Oadd
100	(Expr (Evar (ident_of_nat 13))
101	(Tpointer Any (Tint I16 Signed )))
102	(Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed )))
103	(Tpointer Any (Tint I16 Signed ))))
104	(Ssequence
105	(Sassign (Expr (Evar (ident_of_nat 14))
106	(Tpointer Any (Tint I16 Signed )))
107	(Expr (Evar (ident_of_nat 20))
108	(Tpointer Any (Tint I16 Signed ))))
109	(Ssequence
110	(Sassign (Expr (Evar (ident_of_nat 20))
111	(Tpointer Any (Tint I16 Signed )))
112	(Expr (Ebinop Oadd
113	(Expr (Evar (ident_of_nat 14))
114	(Tpointer Any (Tint I16 Signed )))
115	(Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed )))
116	(Tpointer Any (Tint I16 Signed ))))
117	(Sassign (Expr (Ederef
118	(Expr (Evar (ident_of_nat 13))
119	(Tpointer Any (Tint I16 Signed ))))
120	(Tint I16 Signed ))
121	(Expr (Ederef
122	(Expr (Evar (ident_of_nat 14))
123	(Tpointer Any (Tint I16 Signed ))))
124	(Tint I16 Signed )))))))
125	(LScase I32 (repr ? 5)
126	(Ssequence
127	(Sassign (Expr (Evar (ident_of_nat 11))
128	(Tpointer Any (Tint I16 Signed )))
129	(Expr (Evar (ident_of_nat 19))
130	(Tpointer Any (Tint I16 Signed ))))
131	(Ssequence
132	(Sassign (Expr (Evar (ident_of_nat 19))
133	(Tpointer Any (Tint I16 Signed )))
134	(Expr (Ebinop Oadd
135	(Expr (Evar (ident_of_nat 11))
136	(Tpointer Any (Tint I16 Signed )))
137	(Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed )))
138	(Tpointer Any (Tint I16 Signed ))))
139	(Ssequence
140	(Sassign (Expr (Evar (ident_of_nat 12))
141	(Tpointer Any (Tint I16 Signed )))
142	(Expr (Evar (ident_of_nat 20))
143	(Tpointer Any (Tint I16 Signed ))))
144	(Ssequence
145	(Sassign (Expr (Evar (ident_of_nat 20))
146	(Tpointer Any (Tint I16 Signed )))
147	(Expr (Ebinop Oadd
148	(Expr (Evar (ident_of_nat 12))
149	(Tpointer Any (Tint I16 Signed )))
150	(Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed )))
151	(Tpointer Any (Tint I16 Signed ))))
152	(Sassign (Expr (Ederef
153	(Expr (Evar (ident_of_nat 11))
154	(Tpointer Any (Tint I16 Signed ))))
155	(Tint I16 Signed ))
156	(Expr (Ederef
157	(Expr (Evar (ident_of_nat 12))
158	(Tpointer Any (Tint I16 Signed ))))
159	(Tint I16 Signed )))))))
160	(LScase I32 (repr ? 4)
161	(Ssequence
162	(Sassign (Expr (Evar (ident_of_nat 9))
163	(Tpointer Any (Tint I16 Signed )))
164	(Expr (Evar (ident_of_nat 19))
165	(Tpointer Any (Tint I16 Signed ))))
166	(Ssequence
167	(Sassign (Expr (Evar (ident_of_nat 19))
168	(Tpointer Any (Tint I16 Signed )))
169	(Expr (Ebinop Oadd
170	(Expr (Evar (ident_of_nat 9))
171	(Tpointer Any (Tint I16 Signed )))
172	(Expr (Econst_int I32 (repr ? 1))
173	(Tint I32 Signed )))
174	(Tpointer Any (Tint I16 Signed ))))
175	(Ssequence
176	(Sassign (Expr (Evar (ident_of_nat 10))
177	(Tpointer Any (Tint I16 Signed )))
178	(Expr (Evar (ident_of_nat 20))
179	(Tpointer Any (Tint I16 Signed ))))
180	(Ssequence
181	(Sassign (Expr (Evar (ident_of_nat 20))
182	(Tpointer Any (Tint I16 Signed )))
183	(Expr (Ebinop Oadd
184	(Expr (Evar (ident_of_nat 10))
185	(Tpointer Any (Tint I16 Signed )))
186	(Expr (Econst_int I32 (repr ? 1))
187	(Tint I32 Signed )))
188	(Tpointer Any (Tint I16 Signed ))))
189	(Sassign (Expr (Ederef
190	(Expr (Evar (ident_of_nat 9))
191	(Tpointer Any (Tint I16 Signed ))))
192	(Tint I16 Signed ))
193	(Expr (Ederef
194	(Expr (Evar (ident_of_nat 10))
195	(Tpointer Any (Tint I16 Signed ))))
196	(Tint I16 Signed )))))))
197	(LScase I32 (repr ? 3)
198	(Ssequence
199	(Sassign (Expr (Evar (ident_of_nat 7))
200	(Tpointer Any (Tint I16 Signed )))
201	(Expr (Evar (ident_of_nat 19))
202	(Tpointer Any (Tint I16 Signed ))))
203	(Ssequence
204	(Sassign (Expr (Evar (ident_of_nat 19))
205	(Tpointer Any (Tint I16 Signed )))
206	(Expr (Ebinop Oadd
207	(Expr (Evar (ident_of_nat 7))
208	(Tpointer Any (Tint I16 Signed )))
209	(Expr (Econst_int I32 (repr ? 1))
210	(Tint I32 Signed )))
211	(Tpointer Any (Tint I16 Signed ))))
212	(Ssequence
213	(Sassign (Expr (Evar (ident_of_nat 8))
214	(Tpointer Any (Tint I16 Signed )))
215	(Expr (Evar (ident_of_nat 20))
216	(Tpointer Any (Tint I16 Signed ))))
217	(Ssequence
218	(Sassign (Expr (Evar (ident_of_nat 20))
219	(Tpointer Any (Tint I16 Signed )))
220	(Expr (Ebinop Oadd
221	(Expr (Evar (ident_of_nat 8))
222	(Tpointer Any (Tint I16 Signed )))
223	(Expr (Econst_int I32 (repr ? 1))
224	(Tint I32 Signed )))
225	(Tpointer Any (Tint I16 Signed ))))
226	(Sassign (Expr (Ederef
227	(Expr (Evar (ident_of_nat 7))
228	(Tpointer Any (Tint I16 Signed ))))
229	(Tint I16 Signed ))
230	(Expr (Ederef
231	(Expr (Evar (ident_of_nat 8))
232	(Tpointer Any (Tint I16 Signed ))))
233	(Tint I16 Signed )))))))
234	(LScase I32 (repr ? 2)
235	(Ssequence
236	(Sassign (Expr (Evar (ident_of_nat 5))
237	(Tpointer Any (Tint I16 Signed )))
238	(Expr (Evar (ident_of_nat 19))
239	(Tpointer Any (Tint I16 Signed ))))
240	(Ssequence
241	(Sassign (Expr (Evar (ident_of_nat 19))
242	(Tpointer Any (Tint I16 Signed )))
243	(Expr (Ebinop Oadd
244	(Expr (Evar (ident_of_nat 5))
245	(Tpointer Any (Tint I16 Signed )))
246	(Expr (Econst_int I32 (repr ? 1))
247	(Tint I32 Signed )))
248	(Tpointer Any (Tint I16 Signed ))))
249	(Ssequence
250	(Sassign (Expr (Evar (ident_of_nat 6))
251	(Tpointer Any (Tint I16 Signed )))
252	(Expr (Evar (ident_of_nat 20))
253	(Tpointer Any (Tint I16 Signed ))))
254	(Ssequence
255	(Sassign (Expr (Evar (ident_of_nat 20))
256	(Tpointer Any (Tint I16 Signed )))
257	(Expr (Ebinop Oadd
258	(Expr (Evar (ident_of_nat 6))
259	(Tpointer Any (Tint I16 Signed )))
260	(Expr (Econst_int I32 (repr ? 1))
261	(Tint I32 Signed )))
262	(Tpointer Any (Tint I16 Signed ))))
263	(Sassign (Expr (Ederef
264	(Expr (Evar (ident_of_nat 5))
265	(Tpointer Any (Tint I16 Signed ))))
266	(Tint I16 Signed ))
267	(Expr (Ederef
268	(Expr (Evar (ident_of_nat 6))
269	(Tpointer Any (Tint I16 Signed ))))
270	(Tint I16 Signed )))))))
271	(LScase I32 (repr ? 1)
272	(Ssequence
273	(Sassign (Expr (Evar (ident_of_nat 3))
274	(Tpointer Any (Tint I16 Signed )))
275	(Expr (Evar (ident_of_nat 19))
276	(Tpointer Any (Tint I16 Signed ))))
277	(Ssequence
278	(Sassign (Expr (Evar (ident_of_nat 19))
279	(Tpointer Any (Tint I16 Signed )))
280	(Expr (Ebinop Oadd
281	(Expr (Evar (ident_of_nat 3))
282	(Tpointer Any (Tint I16 Signed )))
283	(Expr (Econst_int I32 (repr ? 1))
284	(Tint I32 Signed )))
285	(Tpointer Any (Tint I16 Signed ))))
286	(Ssequence
287	(Sassign (Expr (Evar (ident_of_nat 4))
288	(Tpointer Any (Tint I16 Signed )))
289	(Expr (Evar (ident_of_nat 20))
290	(Tpointer Any (Tint I16 Signed ))))
291	(Ssequence
292	(Sassign (Expr (Evar (ident_of_nat 20))
293	(Tpointer Any (Tint I16 Signed )))
294	(Expr (Ebinop Oadd
295	(Expr (Evar (ident_of_nat 4))
296	(Tpointer Any (Tint I16 Signed )))
297	(Expr (Econst_int I32 (repr ? 1))
298	(Tint I32 Signed )))
299	(Tpointer Any (Tint I16 Signed ))))
300	(Ssequence
301	(Sassign (Expr (Ederef
302	(Expr (Evar (ident_of_nat 3))
303	(Tpointer Any (Tint I16 Signed ))))
304	(Tint I16 Signed ))
305	(Expr (Ederef
306	(Expr (Evar (ident_of_nat 4))
307	(Tpointer Any (Tint I16 Signed ))))
308	(Tint I16 Signed )))
309	(Ssequence
310	(Sassign (Expr (Evar (ident_of_nat 2))
311	(Tint I32 Signed ))
312	(Expr (Ebinop Osub
313	(Expr (Evar (ident_of_nat 1))
314	(Tint I32 Signed ))
315	(Expr (Econst_int I32 (repr ? 1))
316	(Tint I32 Signed ))) (Tint I32 Signed )))
317	(Ssequence
318	(Sassign (Expr (Evar (ident_of_nat 1))
319	(Tint I32 Signed ))
320	(Expr (Evar (ident_of_nat 2))
321	(Tint I32 Signed )))
322	(Sifthenelse (Expr (Ebinop Ogt
323	(Expr (Evar (ident_of_nat 2))
324	(Tint I32 Signed ))
325	(Expr (Econst_int I32 (repr ? 0))
326	(Tint I32 Signed )))
327	(Tint I32 Signed ))
328	(Sgoto (ident_of_nat 22))
329	Sskip))))))))
330	(LSdefault
331	Sskip)))))))))
332	)))
333
334
335
336	)〉;
337	〈ident_of_nat 23 (* main *), CL_Internal (
338	mk_function (Tint I32 Signed ) [] [〈ident_of_nat 24, (Tarray Any (Tint I16 Signed ) 3)〉 ; 〈ident_of_nat 25, (Tarray Any (Tint I16 Signed ) 3)〉 ]
339	(Ssequence
340	(Sassign (Expr (Ederef
341	(Expr (Ebinop Oadd
342	(Expr (Evar (ident_of_nat 24))
343	(Tarray Any (Tint I16 Signed ) 3))
344	(Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed )))
345	(Tpointer Any (Tint I16 Signed ))))
346	(Tint I16 Signed ))
347	(Expr (Ecast (Tint I16 Signed )
348	(Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed )))
349	(Tint I16 Signed )))
350	(Ssequence
351	(Sassign (Expr (Ederef
352	(Expr (Ebinop Oadd
353	(Expr (Evar (ident_of_nat 24))
354	(Tarray Any (Tint I16 Signed ) 3))
355	(Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed )))
356	(Tpointer Any (Tint I16 Signed ))))
357	(Tint I16 Signed ))
358	(Expr (Ecast (Tint I16 Signed )
359	(Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed )))
360	(Tint I16 Signed )))
361	(Ssequence
362	(Sassign (Expr (Ederef
363	(Expr (Ebinop Oadd
364	(Expr (Evar (ident_of_nat 24))
365	(Tarray Any (Tint I16 Signed ) 3))
366	(Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed )))
367	(Tpointer Any (Tint I16 Signed ))))
368	(Tint I16 Signed ))
369	(Expr (Ecast (Tint I16 Signed )
370	(Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed )))
371	(Tint I16 Signed )))
372	(Ssequence
373	(Scall (None expr) (Expr (Evar (ident_of_nat 0))
374	(Tfunction (Tcons (Tpointer Any (Tint I16 Signed )) (Tcons (Tpointer Any (Tint I16 Signed )) (Tcons (Tint I32 Signed ) Tnil))) Tvoid))
375	[(Expr (Evar (ident_of_nat 25)) (Tarray Any (Tint I16 Signed ) 3));
376	(Expr (Evar (ident_of_nat 24)) (Tarray Any (Tint I16 Signed ) 3));
377	(Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed ))])
378	(Sreturn (Some expr (Expr (Ebinop Oadd
379	(Expr (Ebinop Oadd
380	(Expr (Ecast (Tint I32 Signed )
381	(Expr (Ederef
382	(Expr (Ebinop Oadd
383	(Expr (Evar (ident_of_nat 25))
384	(Tarray Any (Tint I16 Signed ) 3))
385	(Expr (Econst_int I32 (repr ? 0))
386	(Tint I32 Signed )))
387	(Tpointer Any (Tint I16 Signed ))))
388	(Tint I16 Signed )))
389	(Tint I32 Signed ))
390	(Expr (Ecast (Tint I32 Signed )
391	(Expr (Ederef
392	(Expr (Ebinop Oadd
393	(Expr (Evar (ident_of_nat 25))
394	(Tarray Any (Tint I16 Signed ) 3))
395	(Expr (Econst_int I32 (repr ? 1))
396	(Tint I32 Signed )))
397	(Tpointer Any (Tint I16 Signed ))))
398	(Tint I16 Signed )))
399	(Tint I32 Signed ))) (Tint I32 Signed ))
400	(Expr (Ecast (Tint I32 Signed )
401	(Expr (Ederef
402	(Expr (Ebinop Oadd
403	(Expr (Evar (ident_of_nat 25))
404	(Tarray Any (Tint I16 Signed ) 3))
405	(Expr (Econst_int I32 (repr ? 2))
406	(Tint I32 Signed )))
407	(Tpointer Any (Tint I16 Signed ))))
408	(Tint I16 Signed ))) (Tint I32 Signed )))
409	(Tint I32 Signed ))))))))
410
411
412
413	)〉]
414	(ident_of_nat 23)
415
416	.
417
418	(*
419	example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
420	normalize (* you can examine the result here *)
421	*)

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format