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

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

Fix up Clight examples.

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