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

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

Do some light manual disambiguation to make Clight examples go through more
easily.

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