source: src/Clight/test/endptr.c.ma @ 2771

Last change on this file since 2771 was 2393, checked in by campbell, 7 years ago

A pointer comparison test case that illustrates a bug.

File size: 9.2 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
5  [][〈ident_of_nat 0 (* main *), CL_Internal (
6       mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ; 〈ident_of_nat 4, (Tpointer (Tint I32 Signed  ))〉 ; 〈ident_of_nat 5, (Tpointer (Tint I32 Signed  ))〉 ; 〈ident_of_nat 6, (Tpointer (Tint I32 Signed  ))〉 ; 〈ident_of_nat 7, (Tpointer (Tint I32 Signed  ))〉 ; 〈ident_of_nat 8, (Tpointer (Tint I32 Signed  ))〉 ; 〈ident_of_nat 9, (Tpointer (Tint I32 Signed  ))〉 ]
7         (Ssequence
8         (Sassign (Expr (Evar (ident_of_nat 4))
9                    (Tpointer (Tint I32 Signed  )))
10           (Expr (Eaddrof (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
11             (Tpointer (Tint I32 Signed  ))))
12         (Ssequence
13         (Sassign (Expr (Evar (ident_of_nat 5))
14                    (Tpointer (Tint I32 Signed  )))
15           (Expr (Eaddrof (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
16             (Tpointer (Tint I32 Signed  ))))
17         (Ssequence
18         (Sassign (Expr (Evar (ident_of_nat 6))
19                    (Tpointer (Tint I32 Signed  )))
20           (Expr (Eaddrof (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))
21             (Tpointer (Tint I32 Signed  ))))
22         (Ssequence
23         (Sassign (Expr (Evar (ident_of_nat 7))
24                    (Tpointer (Tint I32 Signed  )))
25           (Expr (Ebinop Oadd
26             (Expr (Eaddrof
27               (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
28               (Tpointer (Tint I32 Signed  )))
29             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
30             (Tpointer (Tint I32 Signed  ))))
31         (Ssequence
32         (Sassign (Expr (Evar (ident_of_nat 8))
33                    (Tpointer (Tint I32 Signed  )))
34           (Expr (Ebinop Oadd
35             (Expr (Eaddrof
36               (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
37               (Tpointer (Tint I32 Signed  )))
38             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
39             (Tpointer (Tint I32 Signed  ))))
40         (Ssequence
41         (Sassign (Expr (Evar (ident_of_nat 9))
42                    (Tpointer (Tint I32 Signed  )))
43           (Expr (Ebinop Oadd
44             (Expr (Eaddrof
45               (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))
46               (Tpointer (Tint I32 Signed  )))
47             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
48             (Tpointer (Tint I32 Signed  ))))
49         (Ssequence
50         (Sifthenelse (Expr (Eorbool (Expr (Eorbool (Expr (Ebinop One
51                                                      (Expr (Ebinop Osub
52                                                        (Expr (Evar (ident_of_nat 7))
53                                                          (Tpointer (Tint I32 Signed  )))
54                                                        (Expr (Evar (ident_of_nat 4))
55                                                          (Tpointer (Tint I32 Signed  ))))
56                                                        (Tint I32 Signed  ))
57                                                      (Expr (Econst_int I32 (repr ? 1))
58                                                        (Tint I32 Signed  )))
59                                                      (Tint I32 Signed  ))
60                                       (Expr (Ebinop One
61                                         (Expr (Ebinop Osub
62                                           (Expr (Evar (ident_of_nat 8))
63                                             (Tpointer (Tint I32 Signed  )))
64                                           (Expr (Evar (ident_of_nat 5))
65                                             (Tpointer (Tint I32 Signed  ))))
66                                           (Tint I32 Signed  ))
67                                         (Expr (Econst_int I32 (repr ? 1))
68                                           (Tint I32 Signed  )))
69                                         (Tint I32 Signed  )))
70                                       (Tint I32 Signed  ))
71                        (Expr (Ebinop One
72                          (Expr (Ebinop Osub
73                            (Expr (Evar (ident_of_nat 9))
74                              (Tpointer (Tint I32 Signed  )))
75                            (Expr (Evar (ident_of_nat 6))
76                              (Tpointer (Tint I32 Signed  ))))
77                            (Tint I32 Signed  ))
78                          (Expr (Econst_int I32 (repr ? 1))
79                            (Tint I32 Signed  ))) (Tint I32 Signed  )))
80                        (Tint I32 Signed  ))
81           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 1))
82                                 (Tint I32 Signed  ))))
83           Sskip)
84         (Ssequence
85         (Sifthenelse (Expr (Eorbool (Expr (Ebinop Oeq
86                                       (Expr (Evar (ident_of_nat 5))
87                                         (Tpointer (Tint I32 Signed  )))
88                                       (Expr (Evar (ident_of_nat 8))
89                                         (Tpointer (Tint I32 Signed  ))))
90                                       (Tint I32 Signed  ))
91                        (Expr (Ebinop One
92                          (Expr (Ebinop Oadd
93                            (Expr (Evar (ident_of_nat 5))
94                              (Tpointer (Tint I32 Signed  )))
95                            (Expr (Econst_int I32 (repr ? 1))
96                              (Tint I32 Signed  )))
97                            (Tpointer (Tint I32 Signed  )))
98                          (Expr (Evar (ident_of_nat 8))
99                            (Tpointer (Tint I32 Signed  ))))
100                          (Tint I32 Signed  ))) (Tint I32 Signed  ))
101           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 2))
102                                 (Tint I32 Signed  ))))
103           Sskip)
104         (Ssequence
105         (Sifthenelse (Expr (Eorbool (Expr (Eorbool (Expr (Eorbool (Expr (Eorbool
106                                                                    (Expr (Ebinop
107                                                                    Oeq
108                                                                    (Expr (Evar (ident_of_nat 7))
109                                                                    (Tpointer (Tint I32 Signed  )))
110                                                                    (Expr (Evar (ident_of_nat 5))
111                                                                    (Tpointer (Tint I32 Signed  ))))
112                                                                    (Tint I32 Signed  ))
113                                                                    (Expr (Ebinop
114                                                                    Oeq
115                                                                    (Expr (Evar (ident_of_nat 8))
116                                                                    (Tpointer (Tint I32 Signed  )))
117                                                                    (Expr (Evar (ident_of_nat 6))
118                                                                    (Tpointer (Tint I32 Signed  ))))
119                                                                    (Tint I32 Signed  )))
120                                                                    (Tint I32 Signed  ))
121                                                      (Expr (Ebinop Oeq
122                                                        (Expr (Evar (ident_of_nat 8))
123                                                          (Tpointer (Tint I32 Signed  )))
124                                                        (Expr (Evar (ident_of_nat 4))
125                                                          (Tpointer (Tint I32 Signed  ))))
126                                                        (Tint I32 Signed  )))
127                                                      (Tint I32 Signed  ))
128                                       (Expr (Ebinop Oeq
129                                         (Expr (Evar (ident_of_nat 8))
130                                           (Tpointer (Tint I32 Signed  )))
131                                         (Expr (Evar (ident_of_nat 9))
132                                           (Tpointer (Tint I32 Signed  ))))
133                                         (Tint I32 Signed  )))
134                                       (Tint I32 Signed  ))
135                        (Expr (Ebinop Oeq
136                          (Expr (Evar (ident_of_nat 8))
137                            (Tpointer (Tint I32 Signed  )))
138                          (Expr (Evar (ident_of_nat 7))
139                            (Tpointer (Tint I32 Signed  ))))
140                          (Tint I32 Signed  ))) (Tint I32 Signed  ))
141           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 3))
142                                 (Tint I32 Signed  ))))
143           Sskip)
144         (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 4))
145                               (Tint I32 Signed  )))))))))))))
146       
147       
148       
149     )〉]
150  (ident_of_nat 0)
151 
152.
153
154(*
155example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
156normalize  (* you can examine the result here *)
157*)
Note: See TracBrowser for help on using the repository browser.