source: src/Clight/test/duff.ma @ 725

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

Do some light manual disambiguation to make Clight examples go through more
easily.

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