source: src/Clight/test/search.ma @ 726

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

Change identifiers to Words in Clight and RTLabs semantics.

File size: 9.3 KB
Line 
1include "Clight/Animation.ma".
2
3definition myprog := mk_program clight_fundef type
4  [〈ident_of_nat 0 (* search *), CL_Internal (
5     mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer Any (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 )〉 ]
6       (Ssequence
7       (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
8         (Expr (Ecast (Tint I8 Unsigned )
9           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
10           (Tint I8 Unsigned )))
11       (Ssequence
12       (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
13         (Expr (Ecast (Tint I8 Unsigned )
14           (Expr (Ebinop Osub
15             (Expr (Ecast (Tint I32 Signed  )
16               (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
17               (Tint I32 Signed  ))
18             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
19             (Tint I32 Signed  ))) (Tint I8 Unsigned )))
20       (Ssequence
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 (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 Any (Tint I8 Unsigned )))
49                              (Expr (Evar (ident_of_nat 3))
50                                (Tint I8 Unsigned )))
51                              (Tpointer Any (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 Any (Tint I8 Unsigned )))
67                              (Expr (Evar (ident_of_nat 3))
68                                (Tint I8 Unsigned )))
69                              (Tpointer Any (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 (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 Any (Tint I8 Unsigned )))
90                              (Expr (Evar (ident_of_nat 3))
91                                (Tint I8 Unsigned )))
92                              (Tpointer Any (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 (repr 1)) (Tint I32 Signed  )))
105                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
106           Sskip)))))
107       Sskip)
108       (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
109                             (Expr (Eunop Oneg (Expr (Econst_int (repr 1))
110                                                 (Tint I32 Signed  )))
111                               (Tint I32 Signed  ))) (Tint I8 Unsigned )))))))
112     
113     
114     
115   )〉;
116  〈ident_of_nat 7 (* main *), CL_Internal (
117    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈ident_of_nat 8, (Tint I8 Unsigned )〉 ]
118      (Ssequence
119      (Sassign (Expr (Ederef
120                 (Expr (Ebinop Oadd
121                   (Expr (Evar (ident_of_nat 4))
122                     (Tarray Any (Tint I8 Unsigned ) 5))
123                   (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
124                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
125        (Expr (Ecast (Tint I8 Unsigned )
126          (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
127          (Tint I8 Unsigned )))
128      (Ssequence
129      (Sassign (Expr (Ederef
130                 (Expr (Ebinop Oadd
131                   (Expr (Evar (ident_of_nat 4))
132                     (Tarray Any (Tint I8 Unsigned ) 5))
133                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
134                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
135        (Expr (Ecast (Tint I8 Unsigned )
136          (Expr (Econst_int (repr 18)) (Tint I32 Signed  )))
137          (Tint I8 Unsigned )))
138      (Ssequence
139      (Sassign (Expr (Ederef
140                 (Expr (Ebinop Oadd
141                   (Expr (Evar (ident_of_nat 4))
142                     (Tarray Any (Tint I8 Unsigned ) 5))
143                   (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
144                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
145        (Expr (Ecast (Tint I8 Unsigned )
146          (Expr (Econst_int (repr 23)) (Tint I32 Signed  )))
147          (Tint I8 Unsigned )))
148      (Ssequence
149      (Sassign (Expr (Ederef
150                 (Expr (Ebinop Oadd
151                   (Expr (Evar (ident_of_nat 4))
152                     (Tarray Any (Tint I8 Unsigned ) 5))
153                   (Expr (Econst_int (repr 3)) (Tint I32 Signed  )))
154                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
155        (Expr (Ecast (Tint I8 Unsigned )
156          (Expr (Econst_int (repr 57)) (Tint I32 Signed  )))
157          (Tint I8 Unsigned )))
158      (Ssequence
159      (Sassign (Expr (Ederef
160                 (Expr (Ebinop Oadd
161                   (Expr (Evar (ident_of_nat 4))
162                     (Tarray Any (Tint I8 Unsigned ) 5))
163                   (Expr (Econst_int (repr 4)) (Tint I32 Signed  )))
164                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
165        (Expr (Ecast (Tint I8 Unsigned )
166          (Expr (Econst_int (repr 120)) (Tint I32 Signed  )))
167          (Tint I8 Unsigned )))
168      (Ssequence
169      (Scall (Some expr (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned )))
170        (Expr (Evar (ident_of_nat 0))
171          (Tfunction (Tcons (Tpointer Any (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I8 Unsigned )))
172        [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));
173        (Expr (Ecast (Tint I8 Unsigned )
174          (Expr (Econst_int (repr 5)) (Tint I32 Signed  )))
175          (Tint I8 Unsigned ));
176        (Expr (Ecast (Tint I8 Unsigned )
177          (Expr (Econst_int (repr 57)) (Tint I32 Signed  )))
178          (Tint I8 Unsigned ))])
179      (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
180                            (Expr (Evar (ident_of_nat 8))
181                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))))))
182   
183   
184   
185  )〉]
186  (ident_of_nat 7)
187  []
188.
189
190example exec: result ? (exec_up_to myprog 1000 [EVint (repr 0)]).
191normalize  (* you can examine the result here *)
192%
193qed.
Note: See TracBrowser for help on using the repository browser.