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

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

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File size: 19.8 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.
216
217include "Clight/label.ma".
218
219example labelled_exec:
220  (do p ← clight_label myprog;
221   do s ← exec_up_to clight_fullexec p 1000
222     [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)];
223   match s with [ finished t _ _ ⇒ OK ? (remove_costs t) | _ ⇒ Error ? [ ] ]) = OK ?
224[EVextcall (ident_of_nat 11) [EVint (repr 36)] (EVint (repr 0));
225 EVextcall (ident_of_nat 11) [EVint (repr 69)] (EVint (repr 0));
226 EVextcall (ident_of_nat 11) [EVint (repr 102)] (EVint (repr 0));
227 EVextcall (ident_of_nat 11) [EVint (repr 105)] (EVint (repr 0));
228 EVextcall (ident_of_nat 11) [EVint (repr 136)] (EVint (repr 0));
229 EVextcall (ident_of_nat 11) [EVint (repr 234)] (EVint (repr 0));
230 EVextcall (ident_of_nat 11) [EVint (repr 240)] (EVint (repr 0))]
231.
232normalize  (* you can examine the result here *)
233@refl
234qed.
Note: See TracBrowser for help on using the repository browser.