source: Deliverables/D3.1/C-semantics/test/duff.ma @ 415

Last change on this file since 415 was 415, checked in by campbell, 9 years ago

A couple of amusing examples.

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