source: src/Clight/test/insertsort.ma @ 731

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

Common definition for animation semantics, and factor out IO definitions.

File size: 19.0 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program clight_fundef type
5  [〈ident_of_nat 0 (* insert *), CL_Internal (
6     mk_function Tvoid [〈ident_of_nat 2, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ]
7       (Ssequence
8       (Sifthenelse (Expr (Ebinop Oeq
9                      (Expr (Ederef
10                        (Expr (Evar (ident_of_nat 6))
11                          (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
12                        (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
13                      (Expr (Ecast (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))
14                        (Expr (Ecast (Tpointer Any Tvoid)
15                          (Expr (Econst_int (repr 0)) (Tint I32 Unsigned)))
16                          (Tpointer Any Tvoid)))
17                        (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
18                      (Tint I32 Signed  ))
19         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
20           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
21         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
22           (Expr (Ebinop One
23             (Expr (Ebinop Oge
24               (Expr (Ecast (Tint I32 Signed  )
25                 (Expr (Efield (Expr (Ederef
26                                 (Expr (Ederef
27                                   (Expr (Evar (ident_of_nat 6))
28                                     (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
29                                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
30                                 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))
31                   (Tint I8 Unsigned ))) (Tint I32 Signed  ))
32               (Expr (Ecast (Tint I32 Signed  )
33                 (Expr (Efield (Expr (Ederef
34                                 (Expr (Evar (ident_of_nat 2))
35                                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
36                                 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))
37                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
38               (Tint I32 Signed  ))
39             (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
40             (Tint I32 Signed  ))))
41       (Sifthenelse (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
42         (Ssequence
43         (Sassign (Expr (Efield (Expr (Ederef
44                                  (Expr (Evar (ident_of_nat 2))
45                                    (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
46                                  (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
47                    (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
48           (Expr (Ederef
49             (Expr (Evar (ident_of_nat 6))
50               (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
51             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
52         (Sassign (Expr (Ederef
53                    (Expr (Evar (ident_of_nat 6))
54                      (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
55                    (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
56           (Expr (Evar (ident_of_nat 2))
57             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
58         (Scall (None expr) (Expr (Evar (ident_of_nat 0))
59                              (Tfunction (Tcons (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) Tnil)) Tvoid))
60           [(Expr (Evar (ident_of_nat 2))
61              (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))));
62           (Expr (Ecast (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
63             (Expr (Eaddrof
64               (Expr (Efield (Expr (Ederef
65                               (Expr (Ederef
66                                 (Expr (Evar (ident_of_nat 6))
67                                   (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
68                                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
69                               (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
70                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
71               (Tpointer PData (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
72             (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))])))
73     
74     
75     
76   )〉;
77  〈ident_of_nat 7 (* sort *), CL_Internal (
78    mk_function Tvoid [〈ident_of_nat 10, (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 8, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 5, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 9, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ]
79      (Ssequence
80      (Sassign (Expr (Evar (ident_of_nat 5))
81                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
82        (Expr (Ederef
83          (Expr (Evar (ident_of_nat 10))
84            (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
85          (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
86      (Ssequence
87      (Sassign (Expr (Evar (ident_of_nat 9))
88                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
89        (Expr (Ecast (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))
90          (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
91          (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
92      (Ssequence
93      (Ssequence
94      (Swhile (Expr (Evar (ident_of_nat 5))
95                (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
96        (Ssequence
97        (Sassign (Expr (Evar (ident_of_nat 8))
98                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
99          (Expr (Evar (ident_of_nat 5))
100            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
101        (Ssequence
102        (Sassign (Expr (Evar (ident_of_nat 5))
103                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
104          (Expr (Efield (Expr (Ederef
105                          (Expr (Evar (ident_of_nat 5))
106                            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
107                          (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
108            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
109        (Scall (None expr) (Expr (Evar (ident_of_nat 0))
110                             (Tfunction (Tcons (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) Tnil)) Tvoid))
111          [(Expr (Evar (ident_of_nat 8))
112             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))));
113          (Expr (Eaddrof
114            (Expr (Evar (ident_of_nat 9))
115              (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
116            (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))]))))
117      Sskip)
118      (Sassign (Expr (Ederef
119                 (Expr (Evar (ident_of_nat 10))
120                   (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
121                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
122        (Expr (Evar (ident_of_nat 9))
123          (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))))
124   
125   
126   
127  )〉;
128  〈ident_of_nat 11 (* out *), CL_External (ident_of_nat 11) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉;
129  〈ident_of_nat 12 (* main *), CL_Internal (
130    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 13, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ]
131      (Ssequence
132      (Sassign (Expr (Evar (ident_of_nat 13))
133                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
134        (Expr (Eaddrof
135          (Expr (Evar (ident_of_nat 14))
136            (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
137          (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
138      (Ssequence
139      (Scall (None expr) (Expr (Evar (ident_of_nat 7))
140                           (Tfunction (Tcons (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) Tnil) Tvoid))
141        [(Expr (Eaddrof
142           (Expr (Evar (ident_of_nat 13))
143             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
144           (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))])
145      (Ssequence
146      (Ssequence
147      (Swhile (Expr (Evar (ident_of_nat 13))
148                (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
149        (Ssequence
150        (Scall (None expr) (Expr (Evar (ident_of_nat 11))
151                             (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) Tvoid))
152          [(Expr (Efield (Expr (Ederef
153                           (Expr (Evar (ident_of_nat 13))
154                             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
155                           (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))
156             (Tint I8 Unsigned ))])
157        (Sassign (Expr (Evar (ident_of_nat 13))
158                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
159          (Expr (Efield (Expr (Ederef
160                          (Expr (Evar (ident_of_nat 13))
161                            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
162                          (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
163            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))))
164      Sskip)
165      (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))))))
166   
167   
168   
169  )〉]
170  (ident_of_nat 12)
171  [〈〈〈ident_of_nat 15 (* l6 *),
172     [(Init_int8 (repr 69)) ; (Init_space 3) ; (Init_null PData) ;
173     (Init_space 3) ]〉, PData〉,
174     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
175  〈〈〈ident_of_nat 16 (* l5 *),
176    [(Init_int8 (repr 36)) ; (Init_space 3) ;
177    (Init_addrof PData (ident_of_nat 15) (repr 0))]〉, PData〉,
178    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
179  〈〈〈ident_of_nat 17 (* l4 *),
180    [(Init_int8 (repr 136)) ; (Init_space 3) ;
181    (Init_addrof PData (ident_of_nat 16) (repr 0))]〉, PData〉,
182    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
183  〈〈〈ident_of_nat 18 (* l3 *),
184    [(Init_int8 (repr 105)) ; (Init_space 3) ;
185    (Init_addrof PData (ident_of_nat 17) (repr 0))]〉, PData〉,
186    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
187  〈〈〈ident_of_nat 19 (* l2 *),
188    [(Init_int8 (repr 234)) ; (Init_space 3) ;
189    (Init_addrof PData (ident_of_nat 18) (repr 0))]〉, PData〉,
190    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
191  〈〈〈ident_of_nat 20 (* l1 *),
192    [(Init_int8 (repr 240)) ; (Init_space 3) ;
193    (Init_addrof PData (ident_of_nat 19) (repr 0))]〉, PData〉,
194    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
195  〈〈〈ident_of_nat 14 (* l0 *),
196    [(Init_int8 (repr 102)) ; (Init_space 3) ;
197    (Init_addrof PData (ident_of_nat 20) (repr 0))]〉, PData〉,
198    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉]
199.
200
201example exec:
202  (do s ← exec_up_to clight_fullexec myprog 1000
203     [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)];
204   match s with [ finished t _ _ ⇒ OK ? t | _ ⇒ Error ? ]) = OK ?
205[EVextcall (ident_of_nat 11) [EVint (repr 36)] (EVint (repr 0));
206 EVextcall (ident_of_nat 11) [EVint (repr 69)] (EVint (repr 0));
207 EVextcall (ident_of_nat 11) [EVint (repr 102)] (EVint (repr 0));
208 EVextcall (ident_of_nat 11) [EVint (repr 105)] (EVint (repr 0));
209 EVextcall (ident_of_nat 11) [EVint (repr 136)] (EVint (repr 0));
210 EVextcall (ident_of_nat 11) [EVint (repr 234)] (EVint (repr 0));
211 EVextcall (ident_of_nat 11) [EVint (repr 240)] (EVint (repr 0))]
212.
213normalize  (* you can examine the result here *)
214@refl
215qed.
Note: See TracBrowser for help on using the repository browser.