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

Last change on this file since 725 was 725, checked in by campbell, 9 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.