source: Deliverables/D3.3/id-lookup-branch/Clight/test/insertsort.c.ma @ 1153

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

Merge trunk into branch.

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