source: src/Clight/test/search.c.ma

Last change on this file was 2176, checked in by campbell, 7 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.
File size: 9.7 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 (* search *), CL_Internal (
6       mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
7         (Ssequence
8         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
9           (Expr (Ecast (Tint I8 Unsigned )
10             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
11             (Tint I8 Unsigned )))
12         (Ssequence
13         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
14           (Expr (Ecast (Tint I8 Unsigned )
15             (Expr (Ebinop Osub
16               (Expr (Ecast (Tint I32 Signed  )
17                 (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
18                 (Tint I32 Signed  ))
19               (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
20               (Tint I32 Signed  ))) (Tint I8 Unsigned )))
21         (Ssequence
22         (Swhile (Expr (Ebinop Oge
23                   (Expr (Ecast (Tint I32 Signed  )
24                     (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
25                     (Tint I32 Signed  ))
26                   (Expr (Ecast (Tint I32 Signed  )
27                     (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
28                     (Tint I32 Signed  ))) (Tint I32 Signed  ))
29           (Ssequence
30           (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
31             (Expr (Ecast (Tint I8 Unsigned )
32               (Expr (Ebinop Odiv
33                 (Expr (Ebinop Oadd
34                   (Expr (Ecast (Tint I32 Signed  )
35                     (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
36                     (Tint I32 Signed  ))
37                   (Expr (Ecast (Tint I32 Signed  )
38                     (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
39                     (Tint I32 Signed  ))) (Tint I32 Signed  ))
40                 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
41                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
42           (Ssequence
43           (Sifthenelse (Expr (Ebinop Oeq
44                          (Expr (Ecast (Tint I32 Signed  )
45                            (Expr (Ederef
46                              (Expr (Ebinop Oadd
47                                (Expr (Evar (ident_of_nat 4))
48                                  (Tpointer (Tint I8 Unsigned )))
49                                (Expr (Evar (ident_of_nat 3))
50                                  (Tint I8 Unsigned )))
51                                (Tpointer (Tint I8 Unsigned ))))
52                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))
53                          (Expr (Ecast (Tint I32 Signed  )
54                            (Expr (Evar (ident_of_nat 6))
55                              (Tint I8 Unsigned ))) (Tint I32 Signed  )))
56                          (Tint I32 Signed  ))
57             (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
58                                   (Tint I8 Unsigned ))))
59             Sskip)
60           (Ssequence
61           (Sifthenelse (Expr (Ebinop Ogt
62                          (Expr (Ecast (Tint I32 Signed  )
63                            (Expr (Ederef
64                              (Expr (Ebinop Oadd
65                                (Expr (Evar (ident_of_nat 4))
66                                  (Tpointer (Tint I8 Unsigned )))
67                                (Expr (Evar (ident_of_nat 3))
68                                  (Tint I8 Unsigned )))
69                                (Tpointer (Tint I8 Unsigned ))))
70                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))
71                          (Expr (Ecast (Tint I32 Signed  )
72                            (Expr (Evar (ident_of_nat 6))
73                              (Tint I8 Unsigned ))) (Tint I32 Signed  )))
74                          (Tint I32 Signed  ))
75             (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
76               (Expr (Ecast (Tint I8 Unsigned )
77                 (Expr (Ebinop Osub
78                   (Expr (Ecast (Tint I32 Signed  )
79                     (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
80                     (Tint I32 Signed  ))
81                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
82                   (Tint I32 Signed  ))) (Tint I8 Unsigned )))
83             Sskip)
84           (Sifthenelse (Expr (Ebinop Olt
85                          (Expr (Ecast (Tint I32 Signed  )
86                            (Expr (Ederef
87                              (Expr (Ebinop Oadd
88                                (Expr (Evar (ident_of_nat 4))
89                                  (Tpointer (Tint I8 Unsigned )))
90                                (Expr (Evar (ident_of_nat 3))
91                                  (Tint I8 Unsigned )))
92                                (Tpointer (Tint I8 Unsigned ))))
93                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))
94                          (Expr (Ecast (Tint I32 Signed  )
95                            (Expr (Evar (ident_of_nat 6))
96                              (Tint I8 Unsigned ))) (Tint I32 Signed  )))
97                          (Tint I32 Signed  ))
98             (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
99               (Expr (Ecast (Tint I8 Unsigned )
100                 (Expr (Ebinop Oadd
101                   (Expr (Ecast (Tint I32 Signed  )
102                     (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
103                     (Tint I32 Signed  ))
104                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
105                   (Tint I32 Signed  ))) (Tint I8 Unsigned )))
106             Sskip)))))
107         (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
108                               (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1))
109                                                   (Tint I32 Signed  )))
110                                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))))))
111       
112       
113       
114     )〉;
115    〈ident_of_nat 7 (* main *), CL_Internal (
116      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 4, (Tarray (Tint I8 Unsigned ) 5)〉 ; 〈ident_of_nat 8, (Tint I8 Unsigned )〉 ]
117        (Ssequence
118        (Sassign (Expr (Ederef
119                   (Expr (Ebinop Oadd
120                     (Expr (Evar (ident_of_nat 4))
121                       (Tarray (Tint I8 Unsigned ) 5))
122                     (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
123                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
124          (Expr (Ecast (Tint I8 Unsigned )
125            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
126            (Tint I8 Unsigned )))
127        (Ssequence
128        (Sassign (Expr (Ederef
129                   (Expr (Ebinop Oadd
130                     (Expr (Evar (ident_of_nat 4))
131                       (Tarray (Tint I8 Unsigned ) 5))
132                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
133                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
134          (Expr (Ecast (Tint I8 Unsigned )
135            (Expr (Econst_int I32 (repr ? 18)) (Tint I32 Signed  )))
136            (Tint I8 Unsigned )))
137        (Ssequence
138        (Sassign (Expr (Ederef
139                   (Expr (Ebinop Oadd
140                     (Expr (Evar (ident_of_nat 4))
141                       (Tarray (Tint I8 Unsigned ) 5))
142                     (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
143                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
144          (Expr (Ecast (Tint I8 Unsigned )
145            (Expr (Econst_int I32 (repr ? 23)) (Tint I32 Signed  )))
146            (Tint I8 Unsigned )))
147        (Ssequence
148        (Sassign (Expr (Ederef
149                   (Expr (Ebinop Oadd
150                     (Expr (Evar (ident_of_nat 4))
151                       (Tarray (Tint I8 Unsigned ) 5))
152                     (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
153                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
154          (Expr (Ecast (Tint I8 Unsigned )
155            (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
156            (Tint I8 Unsigned )))
157        (Ssequence
158        (Sassign (Expr (Ederef
159                   (Expr (Ebinop Oadd
160                     (Expr (Evar (ident_of_nat 4))
161                       (Tarray (Tint I8 Unsigned ) 5))
162                     (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed  )))
163                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
164          (Expr (Ecast (Tint I8 Unsigned )
165            (Expr (Econst_int I32 (repr ? 120)) (Tint I32 Signed  )))
166            (Tint I8 Unsigned )))
167        (Ssequence
168        (Scall (Some expr (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned )))
169          (Expr (Evar (ident_of_nat 0))
170            (Tfunction (Tcons (Tpointer (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I8 Unsigned )))
171          [(Expr (Evar (ident_of_nat 4)) (Tarray (Tint I8 Unsigned ) 5));
172          (Expr (Ecast (Tint I8 Unsigned )
173            (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
174            (Tint I8 Unsigned ));
175          (Expr (Ecast (Tint I8 Unsigned )
176            (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
177            (Tint I8 Unsigned ))])
178        (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
179                              (Expr (Evar (ident_of_nat 8))
180                                (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))))))
181     
182     
183     
184    )〉]
185  (ident_of_nat 7)
186 
187.
188
189(*
190example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
191normalize  (* you can examine the result here *)
192*)
Note: See TracBrowser for help on using the repository browser.