source: src/Clight/test/insertsort.c.ma @ 1139

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

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

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.