Changeset 2176 for src/Clight/test
- Timestamp:
- Jul 12, 2012, 1:28:28 PM (9 years ago)
- Location:
- src/Clight/test
- Files:
-
- 6 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/test/duff.c.ma
r1513 r2176 4 4 definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type) 5 5 [][〈ident_of_nat 0 (* copy *), CL_Internal ( 6 mk_function Tvoid [〈ident_of_nat 19, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 20, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed )〉 ] [〈ident_of_nat 1, (Tint I32 Signed )〉 ; 〈ident_of_nat 2, (Tint I32 Signed )〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 4, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 7, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 8, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 10, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 11, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 12, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 14, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 15, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 17, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 18, (Tpointer Any(Tint I16 Signed ))〉 ]6 mk_function Tvoid [〈ident_of_nat 19, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 20, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed )〉 ] [〈ident_of_nat 1, (Tint I32 Signed )〉 ; 〈ident_of_nat 2, (Tint I32 Signed )〉 ; 〈ident_of_nat 3, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 4, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 5, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 6, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 7, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 8, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 9, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 10, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 11, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 12, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 13, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 14, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 15, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 16, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 17, (Tpointer (Tint I16 Signed ))〉 ; 〈ident_of_nat 18, (Tpointer (Tint I16 Signed ))〉 ] 7 7 (Ssequence 8 8 (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed )) … … 23 23 (Ssequence 24 24 (Sassign (Expr (Evar (ident_of_nat 17)) 25 (Tpointer Any (Tint I16 Signed ))) 26 (Expr (Evar (ident_of_nat 19)) 27 (Tpointer Any (Tint I16 Signed )))) 25 (Tpointer (Tint I16 Signed ))) 26 (Expr (Evar (ident_of_nat 19)) (Tpointer (Tint I16 Signed )))) 28 27 (Sassign (Expr (Evar (ident_of_nat 19)) 29 (Tpointer Any(Tint I16 Signed )))28 (Tpointer (Tint I16 Signed ))) 30 29 (Expr (Ebinop Oadd 31 30 (Expr (Evar (ident_of_nat 17)) 32 (Tpointer Any(Tint I16 Signed )))31 (Tpointer (Tint I16 Signed ))) 33 32 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 34 (Tpointer Any(Tint I16 Signed )))))33 (Tpointer (Tint I16 Signed ))))) 35 34 (Ssequence 36 35 (Ssequence 37 36 (Sassign (Expr (Evar (ident_of_nat 18)) 38 (Tpointer Any (Tint I16 Signed ))) 39 (Expr (Evar (ident_of_nat 20)) 40 (Tpointer Any (Tint I16 Signed )))) 37 (Tpointer (Tint I16 Signed ))) 38 (Expr (Evar (ident_of_nat 20)) (Tpointer (Tint I16 Signed )))) 41 39 (Sassign (Expr (Evar (ident_of_nat 20)) 42 (Tpointer Any(Tint I16 Signed )))40 (Tpointer (Tint I16 Signed ))) 43 41 (Expr (Ebinop Oadd 44 42 (Expr (Evar (ident_of_nat 18)) 45 (Tpointer Any(Tint I16 Signed )))43 (Tpointer (Tint I16 Signed ))) 46 44 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 47 (Tpointer Any(Tint I16 Signed )))))45 (Tpointer (Tint I16 Signed ))))) 48 46 (Sassign (Expr (Ederef 49 47 (Expr (Evar (ident_of_nat 17)) 50 (Tpointer Any(Tint I16 Signed ))))48 (Tpointer (Tint I16 Signed )))) 51 49 (Tint I16 Signed )) 52 50 (Expr (Ederef 53 51 (Expr (Evar (ident_of_nat 18)) 54 (Tpointer Any(Tint I16 Signed )))) (Tint I16 Signed ))))))52 (Tpointer (Tint I16 Signed )))) (Tint I16 Signed )))))) 55 53 (LScase I32 (repr ? 7) 56 54 (Ssequence 57 55 (Sassign (Expr (Evar (ident_of_nat 15)) 58 (Tpointer Any(Tint I16 Signed )))56 (Tpointer (Tint I16 Signed ))) 59 57 (Expr (Evar (ident_of_nat 19)) 60 (Tpointer Any(Tint I16 Signed ))))58 (Tpointer (Tint I16 Signed )))) 61 59 (Ssequence 62 60 (Sassign (Expr (Evar (ident_of_nat 19)) 63 (Tpointer Any(Tint I16 Signed )))61 (Tpointer (Tint I16 Signed ))) 64 62 (Expr (Ebinop Oadd 65 63 (Expr (Evar (ident_of_nat 15)) 66 (Tpointer Any(Tint I16 Signed )))64 (Tpointer (Tint I16 Signed ))) 67 65 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 68 (Tpointer Any(Tint I16 Signed ))))66 (Tpointer (Tint I16 Signed )))) 69 67 (Ssequence 70 68 (Sassign (Expr (Evar (ident_of_nat 16)) 71 (Tpointer Any(Tint I16 Signed )))69 (Tpointer (Tint I16 Signed ))) 72 70 (Expr (Evar (ident_of_nat 20)) 73 (Tpointer Any(Tint I16 Signed ))))71 (Tpointer (Tint I16 Signed )))) 74 72 (Ssequence 75 73 (Sassign (Expr (Evar (ident_of_nat 20)) 76 (Tpointer Any(Tint I16 Signed )))74 (Tpointer (Tint I16 Signed ))) 77 75 (Expr (Ebinop Oadd 78 76 (Expr (Evar (ident_of_nat 16)) 79 (Tpointer Any(Tint I16 Signed )))77 (Tpointer (Tint I16 Signed ))) 80 78 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 81 (Tpointer Any(Tint I16 Signed ))))79 (Tpointer (Tint I16 Signed )))) 82 80 (Sassign (Expr (Ederef 83 81 (Expr (Evar (ident_of_nat 15)) 84 (Tpointer Any(Tint I16 Signed ))))82 (Tpointer (Tint I16 Signed )))) 85 83 (Tint I16 Signed )) 86 84 (Expr (Ederef 87 85 (Expr (Evar (ident_of_nat 16)) 88 (Tpointer Any (Tint I16 Signed )))) 89 (Tint I16 Signed ))))))) 86 (Tpointer (Tint I16 Signed )))) (Tint I16 Signed ))))))) 90 87 (LScase I32 (repr ? 6) 91 88 (Ssequence 92 89 (Sassign (Expr (Evar (ident_of_nat 13)) 93 (Tpointer Any(Tint I16 Signed )))90 (Tpointer (Tint I16 Signed ))) 94 91 (Expr (Evar (ident_of_nat 19)) 95 (Tpointer Any(Tint I16 Signed ))))92 (Tpointer (Tint I16 Signed )))) 96 93 (Ssequence 97 94 (Sassign (Expr (Evar (ident_of_nat 19)) 98 (Tpointer Any(Tint I16 Signed )))95 (Tpointer (Tint I16 Signed ))) 99 96 (Expr (Ebinop Oadd 100 97 (Expr (Evar (ident_of_nat 13)) 101 (Tpointer Any(Tint I16 Signed )))98 (Tpointer (Tint I16 Signed ))) 102 99 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 103 (Tpointer Any(Tint I16 Signed ))))100 (Tpointer (Tint I16 Signed )))) 104 101 (Ssequence 105 102 (Sassign (Expr (Evar (ident_of_nat 14)) 106 (Tpointer Any(Tint I16 Signed )))103 (Tpointer (Tint I16 Signed ))) 107 104 (Expr (Evar (ident_of_nat 20)) 108 (Tpointer Any(Tint I16 Signed ))))105 (Tpointer (Tint I16 Signed )))) 109 106 (Ssequence 110 107 (Sassign (Expr (Evar (ident_of_nat 20)) 111 (Tpointer Any(Tint I16 Signed )))108 (Tpointer (Tint I16 Signed ))) 112 109 (Expr (Ebinop Oadd 113 110 (Expr (Evar (ident_of_nat 14)) 114 (Tpointer Any(Tint I16 Signed )))111 (Tpointer (Tint I16 Signed ))) 115 112 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 116 (Tpointer Any(Tint I16 Signed ))))113 (Tpointer (Tint I16 Signed )))) 117 114 (Sassign (Expr (Ederef 118 115 (Expr (Evar (ident_of_nat 13)) 119 (Tpointer Any(Tint I16 Signed ))))116 (Tpointer (Tint I16 Signed )))) 120 117 (Tint I16 Signed )) 121 118 (Expr (Ederef 122 119 (Expr (Evar (ident_of_nat 14)) 123 (Tpointer Any (Tint I16 Signed )))) 124 (Tint I16 Signed ))))))) 120 (Tpointer (Tint I16 Signed )))) (Tint I16 Signed ))))))) 125 121 (LScase I32 (repr ? 5) 126 122 (Ssequence 127 123 (Sassign (Expr (Evar (ident_of_nat 11)) 128 (Tpointer Any(Tint I16 Signed )))124 (Tpointer (Tint I16 Signed ))) 129 125 (Expr (Evar (ident_of_nat 19)) 130 (Tpointer Any(Tint I16 Signed ))))126 (Tpointer (Tint I16 Signed )))) 131 127 (Ssequence 132 128 (Sassign (Expr (Evar (ident_of_nat 19)) 133 (Tpointer Any(Tint I16 Signed )))129 (Tpointer (Tint I16 Signed ))) 134 130 (Expr (Ebinop Oadd 135 131 (Expr (Evar (ident_of_nat 11)) 136 (Tpointer Any(Tint I16 Signed )))132 (Tpointer (Tint I16 Signed ))) 137 133 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 138 (Tpointer Any(Tint I16 Signed ))))134 (Tpointer (Tint I16 Signed )))) 139 135 (Ssequence 140 136 (Sassign (Expr (Evar (ident_of_nat 12)) 141 (Tpointer Any(Tint I16 Signed )))137 (Tpointer (Tint I16 Signed ))) 142 138 (Expr (Evar (ident_of_nat 20)) 143 (Tpointer Any(Tint I16 Signed ))))139 (Tpointer (Tint I16 Signed )))) 144 140 (Ssequence 145 141 (Sassign (Expr (Evar (ident_of_nat 20)) 146 (Tpointer Any(Tint I16 Signed )))142 (Tpointer (Tint I16 Signed ))) 147 143 (Expr (Ebinop Oadd 148 144 (Expr (Evar (ident_of_nat 12)) 149 (Tpointer Any(Tint I16 Signed )))145 (Tpointer (Tint I16 Signed ))) 150 146 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 151 (Tpointer Any(Tint I16 Signed ))))147 (Tpointer (Tint I16 Signed )))) 152 148 (Sassign (Expr (Ederef 153 149 (Expr (Evar (ident_of_nat 11)) 154 (Tpointer Any(Tint I16 Signed ))))150 (Tpointer (Tint I16 Signed )))) 155 151 (Tint I16 Signed )) 156 152 (Expr (Ederef 157 153 (Expr (Evar (ident_of_nat 12)) 158 (Tpointer Any(Tint I16 Signed ))))154 (Tpointer (Tint I16 Signed )))) 159 155 (Tint I16 Signed ))))))) 160 156 (LScase I32 (repr ? 4) 161 157 (Ssequence 162 158 (Sassign (Expr (Evar (ident_of_nat 9)) 163 (Tpointer Any(Tint I16 Signed )))159 (Tpointer (Tint I16 Signed ))) 164 160 (Expr (Evar (ident_of_nat 19)) 165 (Tpointer Any(Tint I16 Signed ))))161 (Tpointer (Tint I16 Signed )))) 166 162 (Ssequence 167 163 (Sassign (Expr (Evar (ident_of_nat 19)) 168 (Tpointer Any(Tint I16 Signed )))164 (Tpointer (Tint I16 Signed ))) 169 165 (Expr (Ebinop Oadd 170 166 (Expr (Evar (ident_of_nat 9)) 171 (Tpointer Any(Tint I16 Signed )))167 (Tpointer (Tint I16 Signed ))) 172 168 (Expr (Econst_int I32 (repr ? 1)) 173 169 (Tint I32 Signed ))) 174 (Tpointer Any(Tint I16 Signed ))))170 (Tpointer (Tint I16 Signed )))) 175 171 (Ssequence 176 172 (Sassign (Expr (Evar (ident_of_nat 10)) 177 (Tpointer Any(Tint I16 Signed )))173 (Tpointer (Tint I16 Signed ))) 178 174 (Expr (Evar (ident_of_nat 20)) 179 (Tpointer Any(Tint I16 Signed ))))175 (Tpointer (Tint I16 Signed )))) 180 176 (Ssequence 181 177 (Sassign (Expr (Evar (ident_of_nat 20)) 182 (Tpointer Any(Tint I16 Signed )))178 (Tpointer (Tint I16 Signed ))) 183 179 (Expr (Ebinop Oadd 184 180 (Expr (Evar (ident_of_nat 10)) 185 (Tpointer Any(Tint I16 Signed )))181 (Tpointer (Tint I16 Signed ))) 186 182 (Expr (Econst_int I32 (repr ? 1)) 187 183 (Tint I32 Signed ))) 188 (Tpointer Any(Tint I16 Signed ))))184 (Tpointer (Tint I16 Signed )))) 189 185 (Sassign (Expr (Ederef 190 186 (Expr (Evar (ident_of_nat 9)) 191 (Tpointer Any(Tint I16 Signed ))))187 (Tpointer (Tint I16 Signed )))) 192 188 (Tint I16 Signed )) 193 189 (Expr (Ederef 194 190 (Expr (Evar (ident_of_nat 10)) 195 (Tpointer Any(Tint I16 Signed ))))191 (Tpointer (Tint I16 Signed )))) 196 192 (Tint I16 Signed ))))))) 197 193 (LScase I32 (repr ? 3) 198 194 (Ssequence 199 195 (Sassign (Expr (Evar (ident_of_nat 7)) 200 (Tpointer Any(Tint I16 Signed )))196 (Tpointer (Tint I16 Signed ))) 201 197 (Expr (Evar (ident_of_nat 19)) 202 (Tpointer Any(Tint I16 Signed ))))198 (Tpointer (Tint I16 Signed )))) 203 199 (Ssequence 204 200 (Sassign (Expr (Evar (ident_of_nat 19)) 205 (Tpointer Any(Tint I16 Signed )))201 (Tpointer (Tint I16 Signed ))) 206 202 (Expr (Ebinop Oadd 207 203 (Expr (Evar (ident_of_nat 7)) 208 (Tpointer Any(Tint I16 Signed )))204 (Tpointer (Tint I16 Signed ))) 209 205 (Expr (Econst_int I32 (repr ? 1)) 210 206 (Tint I32 Signed ))) 211 (Tpointer Any(Tint I16 Signed ))))207 (Tpointer (Tint I16 Signed )))) 212 208 (Ssequence 213 209 (Sassign (Expr (Evar (ident_of_nat 8)) 214 (Tpointer Any(Tint I16 Signed )))210 (Tpointer (Tint I16 Signed ))) 215 211 (Expr (Evar (ident_of_nat 20)) 216 (Tpointer Any(Tint I16 Signed ))))212 (Tpointer (Tint I16 Signed )))) 217 213 (Ssequence 218 214 (Sassign (Expr (Evar (ident_of_nat 20)) 219 (Tpointer Any(Tint I16 Signed )))215 (Tpointer (Tint I16 Signed ))) 220 216 (Expr (Ebinop Oadd 221 217 (Expr (Evar (ident_of_nat 8)) 222 (Tpointer Any(Tint I16 Signed )))218 (Tpointer (Tint I16 Signed ))) 223 219 (Expr (Econst_int I32 (repr ? 1)) 224 220 (Tint I32 Signed ))) 225 (Tpointer Any(Tint I16 Signed ))))221 (Tpointer (Tint I16 Signed )))) 226 222 (Sassign (Expr (Ederef 227 223 (Expr (Evar (ident_of_nat 7)) 228 (Tpointer Any(Tint I16 Signed ))))224 (Tpointer (Tint I16 Signed )))) 229 225 (Tint I16 Signed )) 230 226 (Expr (Ederef 231 227 (Expr (Evar (ident_of_nat 8)) 232 (Tpointer Any(Tint I16 Signed ))))228 (Tpointer (Tint I16 Signed )))) 233 229 (Tint I16 Signed ))))))) 234 230 (LScase I32 (repr ? 2) 235 231 (Ssequence 236 232 (Sassign (Expr (Evar (ident_of_nat 5)) 237 (Tpointer Any(Tint I16 Signed )))233 (Tpointer (Tint I16 Signed ))) 238 234 (Expr (Evar (ident_of_nat 19)) 239 (Tpointer Any(Tint I16 Signed ))))235 (Tpointer (Tint I16 Signed )))) 240 236 (Ssequence 241 237 (Sassign (Expr (Evar (ident_of_nat 19)) 242 (Tpointer Any(Tint I16 Signed )))238 (Tpointer (Tint I16 Signed ))) 243 239 (Expr (Ebinop Oadd 244 240 (Expr (Evar (ident_of_nat 5)) 245 (Tpointer Any(Tint I16 Signed )))241 (Tpointer (Tint I16 Signed ))) 246 242 (Expr (Econst_int I32 (repr ? 1)) 247 243 (Tint I32 Signed ))) 248 (Tpointer Any(Tint I16 Signed ))))244 (Tpointer (Tint I16 Signed )))) 249 245 (Ssequence 250 246 (Sassign (Expr (Evar (ident_of_nat 6)) 251 (Tpointer Any(Tint I16 Signed )))247 (Tpointer (Tint I16 Signed ))) 252 248 (Expr (Evar (ident_of_nat 20)) 253 (Tpointer Any(Tint I16 Signed ))))249 (Tpointer (Tint I16 Signed )))) 254 250 (Ssequence 255 251 (Sassign (Expr (Evar (ident_of_nat 20)) 256 (Tpointer Any(Tint I16 Signed )))252 (Tpointer (Tint I16 Signed ))) 257 253 (Expr (Ebinop Oadd 258 254 (Expr (Evar (ident_of_nat 6)) 259 (Tpointer Any(Tint I16 Signed )))255 (Tpointer (Tint I16 Signed ))) 260 256 (Expr (Econst_int I32 (repr ? 1)) 261 257 (Tint I32 Signed ))) 262 (Tpointer Any(Tint I16 Signed ))))258 (Tpointer (Tint I16 Signed )))) 263 259 (Sassign (Expr (Ederef 264 260 (Expr (Evar (ident_of_nat 5)) 265 (Tpointer Any(Tint I16 Signed ))))261 (Tpointer (Tint I16 Signed )))) 266 262 (Tint I16 Signed )) 267 263 (Expr (Ederef 268 264 (Expr (Evar (ident_of_nat 6)) 269 (Tpointer Any(Tint I16 Signed ))))265 (Tpointer (Tint I16 Signed )))) 270 266 (Tint I16 Signed ))))))) 271 267 (LScase I32 (repr ? 1) 272 268 (Ssequence 273 269 (Sassign (Expr (Evar (ident_of_nat 3)) 274 (Tpointer Any(Tint I16 Signed )))270 (Tpointer (Tint I16 Signed ))) 275 271 (Expr (Evar (ident_of_nat 19)) 276 (Tpointer Any(Tint I16 Signed ))))272 (Tpointer (Tint I16 Signed )))) 277 273 (Ssequence 278 274 (Sassign (Expr (Evar (ident_of_nat 19)) 279 (Tpointer Any(Tint I16 Signed )))275 (Tpointer (Tint I16 Signed ))) 280 276 (Expr (Ebinop Oadd 281 277 (Expr (Evar (ident_of_nat 3)) 282 (Tpointer Any(Tint I16 Signed )))278 (Tpointer (Tint I16 Signed ))) 283 279 (Expr (Econst_int I32 (repr ? 1)) 284 280 (Tint I32 Signed ))) 285 (Tpointer Any(Tint I16 Signed ))))281 (Tpointer (Tint I16 Signed )))) 286 282 (Ssequence 287 283 (Sassign (Expr (Evar (ident_of_nat 4)) 288 (Tpointer Any(Tint I16 Signed )))284 (Tpointer (Tint I16 Signed ))) 289 285 (Expr (Evar (ident_of_nat 20)) 290 (Tpointer Any(Tint I16 Signed ))))286 (Tpointer (Tint I16 Signed )))) 291 287 (Ssequence 292 288 (Sassign (Expr (Evar (ident_of_nat 20)) 293 (Tpointer Any(Tint I16 Signed )))289 (Tpointer (Tint I16 Signed ))) 294 290 (Expr (Ebinop Oadd 295 291 (Expr (Evar (ident_of_nat 4)) 296 (Tpointer Any(Tint I16 Signed )))292 (Tpointer (Tint I16 Signed ))) 297 293 (Expr (Econst_int I32 (repr ? 1)) 298 294 (Tint I32 Signed ))) 299 (Tpointer Any(Tint I16 Signed ))))295 (Tpointer (Tint I16 Signed )))) 300 296 (Ssequence 301 297 (Sassign (Expr (Ederef 302 298 (Expr (Evar (ident_of_nat 3)) 303 (Tpointer Any(Tint I16 Signed ))))299 (Tpointer (Tint I16 Signed )))) 304 300 (Tint I16 Signed )) 305 301 (Expr (Ederef 306 302 (Expr (Evar (ident_of_nat 4)) 307 (Tpointer Any(Tint I16 Signed ))))303 (Tpointer (Tint I16 Signed )))) 308 304 (Tint I16 Signed ))) 309 305 (Ssequence … … 336 332 )〉; 337 333 〈ident_of_nat 23 (* main *), CL_Internal ( 338 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 24, (Tarray Any (Tint I16 Signed ) 3)〉 ; 〈ident_of_nat 25, (Tarray Any (Tint I16 Signed ) 3)〉 ]334 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 24, (Tarray (Tint I16 Signed ) 3)〉 ; 〈ident_of_nat 25, (Tarray (Tint I16 Signed ) 3)〉 ] 339 335 (Ssequence 340 336 (Sassign (Expr (Ederef 341 337 (Expr (Ebinop Oadd 342 338 (Expr (Evar (ident_of_nat 24)) 343 (Tarray Any(Tint I16 Signed ) 3))339 (Tarray (Tint I16 Signed ) 3)) 344 340 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 345 (Tpointer Any (Tint I16 Signed )))) 346 (Tint I16 Signed )) 341 (Tpointer (Tint I16 Signed )))) (Tint I16 Signed )) 347 342 (Expr (Ecast (Tint I16 Signed ) 348 343 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) … … 352 347 (Expr (Ebinop Oadd 353 348 (Expr (Evar (ident_of_nat 24)) 354 (Tarray Any(Tint I16 Signed ) 3))349 (Tarray (Tint I16 Signed ) 3)) 355 350 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 356 (Tpointer Any (Tint I16 Signed )))) 357 (Tint I16 Signed )) 351 (Tpointer (Tint I16 Signed )))) (Tint I16 Signed )) 358 352 (Expr (Ecast (Tint I16 Signed ) 359 353 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) … … 363 357 (Expr (Ebinop Oadd 364 358 (Expr (Evar (ident_of_nat 24)) 365 (Tarray Any(Tint I16 Signed ) 3))359 (Tarray (Tint I16 Signed ) 3)) 366 360 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 367 (Tpointer Any (Tint I16 Signed )))) 368 (Tint I16 Signed )) 361 (Tpointer (Tint I16 Signed )))) (Tint I16 Signed )) 369 362 (Expr (Ecast (Tint I16 Signed ) 370 363 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed ))) … … 372 365 (Ssequence 373 366 (Scall (None expr) (Expr (Evar (ident_of_nat 0)) 374 (Tfunction (Tcons (Tpointer Any (Tint I16 Signed )) (Tcons (Tpointer Any(Tint I16 Signed )) (Tcons (Tint I32 Signed ) Tnil))) Tvoid))375 [(Expr (Evar (ident_of_nat 25)) (Tarray Any(Tint I16 Signed ) 3));376 (Expr (Evar (ident_of_nat 24)) (Tarray Any(Tint I16 Signed ) 3));367 (Tfunction (Tcons (Tpointer (Tint I16 Signed )) (Tcons (Tpointer (Tint I16 Signed )) (Tcons (Tint I32 Signed ) Tnil))) Tvoid)) 368 [(Expr (Evar (ident_of_nat 25)) (Tarray (Tint I16 Signed ) 3)); 369 (Expr (Evar (ident_of_nat 24)) (Tarray (Tint I16 Signed ) 3)); 377 370 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed ))]) 378 371 (Sreturn (Some expr (Expr (Ebinop Oadd … … 382 375 (Expr (Ebinop Oadd 383 376 (Expr (Evar (ident_of_nat 25)) 384 (Tarray Any(Tint I16 Signed ) 3))377 (Tarray (Tint I16 Signed ) 3)) 385 378 (Expr (Econst_int I32 (repr ? 0)) 386 379 (Tint I32 Signed ))) 387 (Tpointer Any(Tint I16 Signed ))))380 (Tpointer (Tint I16 Signed )))) 388 381 (Tint I16 Signed ))) 389 382 (Tint I32 Signed )) … … 392 385 (Expr (Ebinop Oadd 393 386 (Expr (Evar (ident_of_nat 25)) 394 (Tarray Any(Tint I16 Signed ) 3))387 (Tarray (Tint I16 Signed ) 3)) 395 388 (Expr (Econst_int I32 (repr ? 1)) 396 389 (Tint I32 Signed ))) 397 (Tpointer Any(Tint I16 Signed ))))390 (Tpointer (Tint I16 Signed )))) 398 391 (Tint I16 Signed ))) 399 392 (Tint I32 Signed ))) (Tint I32 Signed )) … … 402 395 (Expr (Ebinop Oadd 403 396 (Expr (Evar (ident_of_nat 25)) 404 (Tarray Any(Tint I16 Signed ) 3))397 (Tarray (Tint I16 Signed ) 3)) 405 398 (Expr (Econst_int I32 (repr ? 2)) 406 399 (Tint I32 Signed ))) 407 (Tpointer Any(Tint I16 Signed ))))400 (Tpointer (Tint I16 Signed )))) 408 401 (Tint I16 Signed ))) (Tint I32 Signed ))) 409 402 (Tint I32 Signed )))))))) -
src/Clight/test/insertsort.c.ma
r1513 r2176 6 6 7 7 definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type) 8 [〈〈ident_of_nat 3 (* l6 *), Any〉,8 [〈〈ident_of_nat 3 (* l6 *), XData〉, 9 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〉,10 (Init_null) ], 11 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉; 12 〈〈ident_of_nat 4 (* l5 *), XData〉, 13 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〉,14 (Init_addrof (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 (ident_of_nat 0)) Fnil)))〉〉; 16 〈〈ident_of_nat 5 (* l4 *), XData〉, 17 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〉,18 (Init_addrof (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 (ident_of_nat 0)) Fnil)))〉〉; 20 〈〈ident_of_nat 6 (* l3 *), XData〉, 21 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〉,22 (Init_addrof (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 (ident_of_nat 0)) Fnil)))〉〉; 24 〈〈ident_of_nat 7 (* l2 *), XData〉, 25 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〉,26 (Init_addrof (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 (ident_of_nat 0)) Fnil)))〉〉; 28 〈〈ident_of_nat 8 (* l1 *), XData〉, 29 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〉,30 (Init_addrof (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 (ident_of_nat 0)) Fnil)))〉〉; 32 〈〈ident_of_nat 9 (* l0 *), XData〉, 33 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)))〉〉]34 (Init_addrof (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 (ident_of_nat 0)) Fnil)))〉〉] 36 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 )〉 ]37 mk_function Tvoid [〈ident_of_nat 12, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 13, (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 11, (Tint I32 Signed )〉 ] 38 38 (Ssequence 39 39 (Sifthenelse (Expr (Ebinop Oeq 40 40 (Expr (Ederef 41 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))))45 (Expr (Ecast (Tpointer AnyTvoid)42 (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))) 43 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) 44 (Expr (Ecast (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) 45 (Expr (Ecast (Tpointer Tvoid) 46 46 (Expr (Econst_int I8 (repr ? 0)) 47 (Tint I8 Unsigned ))) (Tpointer AnyTvoid)))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))))))47 (Tint I8 Unsigned ))) (Tpointer Tvoid))) 48 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))) 49 49 (Tint I32 Signed )) 50 50 (Sassign (Expr (Evar (ident_of_nat 11)) (Tint I32 Signed )) … … 57 57 (Expr (Ederef 58 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))59 (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))) 60 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 1)) 62 62 (Tint I8 Unsigned ))) (Tint I32 Signed )) 63 63 (Expr (Ecast (Tint I32 Signed ) 64 64 (Expr (Efield (Expr (Ederef 65 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))66 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 1)) 68 68 (Tint I8 Unsigned ))) (Tint I32 Signed ))) 69 69 (Tint I32 Signed )) … … 74 74 (Sassign (Expr (Efield (Expr (Ederef 75 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)))))76 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 2)) 78 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) 79 79 (Expr (Ederef 80 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))))))81 (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))) 82 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))) 83 83 (Sassign (Expr (Ederef 84 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)))))85 (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))) 86 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) 87 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)))))))88 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))) 89 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))90 (Tfunction (Tcons (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid)) 91 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)))));92 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))); 93 93 (Expr (Eaddrof 94 94 (Expr (Efield (Expr (Ederef 95 95 (Expr (Ederef 96 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))))))])))97 (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))) 98 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 2)) 100 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))) 101 (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))]))) 102 102 103 103 … … 105 105 )〉; 106 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))))〉 ]107 mk_function Tvoid [〈ident_of_nat 17, (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 15, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 2, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 16, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ] 108 108 (Ssequence 109 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)))))110 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) 111 111 (Expr (Ederef 112 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))))))113 (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))) 114 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))) 115 115 (Ssequence 116 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))))117 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) 118 (Expr (Ecast (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) 119 119 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 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))))))120 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))) 121 121 (Ssequence 122 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)))))123 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) 124 124 (Ssequence 125 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)))))126 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) 127 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))))))128 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))) 129 129 (Ssequence 130 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)))))131 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) 132 132 (Expr (Efield (Expr (Ederef 133 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))))))134 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 2)) 136 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))) 137 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))138 (Tfunction (Tcons (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid)) 139 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)))));140 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))); 141 141 (Expr (Eaddrof 142 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))))))]))))143 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))) 144 (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))])))) 145 145 (Sassign (Expr (Ederef 146 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)))))147 (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))) 148 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) 149 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)))))))))150 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))))) 151 151 152 152 … … 155 155 〈ident_of_nat 18 (* out *), CL_External (ident_of_nat 18) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉; 156 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))))〉 ]157 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 20, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ] 158 158 (Ssequence 159 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)))))160 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) 161 161 (Expr (Eaddrof 162 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))))))163 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) 164 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))) 165 165 (Ssequence 166 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))167 (Tfunction (Tcons (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) Tnil) Tvoid)) 168 168 [(Expr (Eaddrof 169 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))))))])170 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))) 171 (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))]) 172 172 (Ssequence 173 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)))))174 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) 175 175 (Ssequence 176 176 (Scall (None expr) (Expr (Evar (ident_of_nat 18)) … … 178 178 [(Expr (Efield (Expr (Ederef 179 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))180 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 1)) 182 182 (Tint I8 Unsigned ))]) 183 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)))))184 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) 185 185 (Expr (Efield (Expr (Ederef 186 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))))))))187 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 2)) 189 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))) 190 190 (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0)) 191 191 (Tint I32 Signed ))))))) -
src/Clight/test/memorymodel.ma
r1993 r2176 21 21 store. *) 22 22 definition store0 := empty. 23 definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 Any.23 definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 XData. 24 24 definition store1 : mem ≝ fst ?? store1block. 25 25 definition block :block := pi1 … (snd ?? store1block). … … 27 27 (* write a value *) 28 28 definition store2 : mem. 29 letin r ≝ (store (ASTint I16 Unsigned) store1 (mk_pointer Any block (same_compat …) zero_offset) (Vint I16 (repr ? 1)));29 letin r ≝ (store (ASTint I16 Unsigned) store1 (mk_pointer block zero_offset) (Vint I16 (repr ? 1))) 30 30 31 31 lapply (refl ? r); elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct … … 34 34 (* overwrite the first byte of the value *) 35 35 definition store3 : mem. 36 letin r ≝ (store (ASTint I8 Unsigned) store2 (mk_pointer Any block (same_compat …) zero_offset) (Vint I8 (repr ? 1)));36 letin r ≝ (store (ASTint I8 Unsigned) store2 (mk_pointer block zero_offset) (Vint I8 (repr ? 1))) 37 37 38 38 lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct … … 41 41 (* This is what happened under the original CompCert 1.6 ported memory model: 42 42 The size checking rejects the read and gives us Some Vundef. 43 example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …)zero_offset) = Some ? Vundef. @refl qed.43 example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? Vundef. @refl qed. 44 44 *) 45 45 (* Now we do byte-wise values and get to see the altered integer. *) 46 example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …)zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed.46 example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed. 47 47 48 48 (* The read is successful and returns the value. *) 49 example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer Any block (same_compat …)zero_offset) = Some ? (Vint I8 (repr ? 1)). // qed.49 example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer block zero_offset) = Some ? (Vint I8 (repr ? 1)). // qed. 50 50 51 51 (* NB: Double frees are allowed by the memory model (although not necessarily … … 57 57 stack memory in the semantics. *) 58 58 definition storeA := empty. 59 definition storeBblkB := alloc storeA 0 4 Any.60 definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.59 definition storeBblkB := alloc storeA 0 4 XData. 60 definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 XData. 61 61 definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB). 62 62 definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)). … … 67 67 doesn't currently expose parts of pointers. *) 68 68 definition storeI := empty. 69 definition storeIIblk := alloc storeI 0 4 Any.69 definition storeIIblk := alloc storeI 0 4 XData. 70 70 definition storeIII : mem. 71 letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset) (Vint I32 (repr ? 1)));71 letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer (snd ?? storeIIblk) zero_offset) (Vint I32 (repr ? 1))); 72 72 lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct 73 73 | #rr #_ @rr ] qed. 74 definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset).74 definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer (snd ?? storeIIblk) zero_offset). 75 75 example byteundef: byte = Some ? (Vint I8 (repr ? 0)). // qed. (* :) *) 76 -
src/Clight/test/null-op.c.ma
r1513 r2176 4 4 definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type) 5 5 [][〈ident_of_nat 0 (* main *), CL_Internal ( 6 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer Any(Tint I8 Unsigned ))〉 ]6 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tpointer (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer (Tint I8 Unsigned ))〉 ] 7 7 (Ssequence 8 8 (Sassign (Expr (Evar (ident_of_nat 2)) 9 (Tpointer Any(Tint I8 Unsigned )))10 (Expr (Ecast (Tpointer Any(Tint I8 Unsigned ))9 (Tpointer (Tint I8 Unsigned ))) 10 (Expr (Ecast (Tpointer (Tint I8 Unsigned )) 11 11 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 12 (Tpointer Any(Tint I8 Unsigned ))))12 (Tpointer (Tint I8 Unsigned )))) 13 13 (Ssequence 14 14 (Sassign (Expr (Evar (ident_of_nat 3)) 15 (Tpointer Any(Tint I8 Unsigned )))15 (Tpointer (Tint I8 Unsigned ))) 16 16 (Expr (Eaddrof (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))) 17 (Tpointer Any(Tint I8 Unsigned ))))17 (Tpointer (Tint I8 Unsigned )))) 18 18 (Ssequence 19 19 (Sifthenelse (Expr (Ebinop Oeq 20 20 (Expr (Evar (ident_of_nat 2)) 21 (Tpointer Any(Tint I8 Unsigned )))21 (Tpointer (Tint I8 Unsigned ))) 22 22 (Expr (Evar (ident_of_nat 3)) 23 (Tpointer Any(Tint I8 Unsigned ))))23 (Tpointer (Tint I8 Unsigned )))) 24 24 (Tint I32 Signed )) 25 25 (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0)) … … 30 30 (Expr (Ebinop Osub 31 31 (Expr (Evar (ident_of_nat 2)) 32 (Tpointer Any(Tint I8 Unsigned )))32 (Tpointer (Tint I8 Unsigned ))) 33 33 (Expr (Evar (ident_of_nat 2)) 34 (Tpointer Any(Tint I8 Unsigned ))))34 (Tpointer (Tint I8 Unsigned )))) 35 35 (Tint I32 Signed )) 36 36 (Expr (Econst_int I32 (repr ? 0)) … … 41 41 (Ssequence 42 42 (Sassign (Expr (Evar (ident_of_nat 2)) 43 (Tpointer Any(Tint I8 Unsigned )))43 (Tpointer (Tint I8 Unsigned ))) 44 44 (Expr (Ebinop Oadd 45 (Expr (Evar (ident_of_nat 2)) 46 (Tpointer Any (Tint I8 Unsigned ))) 45 (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned ))) 47 46 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 48 (Tpointer Any(Tint I8 Unsigned ))))47 (Tpointer (Tint I8 Unsigned )))) 49 48 (Ssequence 50 49 (Sassign (Expr (Evar (ident_of_nat 2)) 51 (Tpointer Any(Tint I8 Unsigned )))50 (Tpointer (Tint I8 Unsigned ))) 52 51 (Expr (Ebinop Oadd 53 52 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed )) 54 (Expr (Evar (ident_of_nat 2)) 55 (Tpointer Any (Tint I8 Unsigned )))) 56 (Tpointer Any (Tint I8 Unsigned )))) 53 (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned )))) 54 (Tpointer (Tint I8 Unsigned )))) 57 55 (Ssequence 58 56 (Sassign (Expr (Evar (ident_of_nat 2)) 59 (Tpointer Any(Tint I8 Unsigned )))57 (Tpointer (Tint I8 Unsigned ))) 60 58 (Expr (Ebinop Osub 61 (Expr (Evar (ident_of_nat 2)) 62 (Tpointer Any (Tint I8 Unsigned ))) 59 (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned ))) 63 60 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 64 (Tpointer Any(Tint I8 Unsigned ))))61 (Tpointer (Tint I8 Unsigned )))) 65 62 (Sreturn (Some expr (Expr (Ebinop Oeq 66 63 (Expr (Evar (ident_of_nat 2)) 67 (Tpointer Any(Tint I8 Unsigned )))68 (Expr (Ecast (Tpointer Any(Tint I8 Unsigned ))69 (Expr (Ecast (Tpointer AnyTvoid)64 (Tpointer (Tint I8 Unsigned ))) 65 (Expr (Ecast (Tpointer (Tint I8 Unsigned )) 66 (Expr (Ecast (Tpointer Tvoid) 70 67 (Expr (Econst_int I8 (repr ? 0)) 71 (Tint I8 Unsigned ))) 72 (Tpointer Any Tvoid))) 73 (Tpointer Any (Tint I8 Unsigned )))) 68 (Tint I8 Unsigned ))) (Tpointer Tvoid))) 69 (Tpointer (Tint I8 Unsigned )))) 74 70 (Tint I32 Signed ))))))))))) 75 71 -
src/Clight/test/search.c.ma
r1991 r2176 2 2 include "common/Animation.ma". 3 3 4 definition myprog := mk_program (λ_.clight_fundef) ((list init_data) × type) 5 [] 6 [〈ident_of_nat 0 (* search *), CL_Internal ( 7 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 )〉 ] 8 (Ssequence 9 (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )) 10 (Expr (Ecast (Tint I8 Unsigned ) 11 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 12 (Tint I8 Unsigned ))) 13 (Ssequence 14 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 15 (Expr (Ecast (Tint I8 Unsigned ) 16 (Expr (Ebinop Osub 17 (Expr (Ecast (Tint I32 Signed ) 18 (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned ))) 19 (Tint I32 Signed )) 20 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 21 (Tint I32 Signed ))) (Tint I8 Unsigned ))) 22 (Ssequence 23 (Swhile (Expr (Ebinop Oge 24 (Expr (Ecast (Tint I32 Signed ) 25 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 26 (Tint I32 Signed )) 27 (Expr (Ecast (Tint I32 Signed ) 28 (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))) 29 (Tint I32 Signed ))) (Tint I32 Signed )) 4 definition 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 )〉 ] 30 7 (Ssequence 31 (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))8 (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )) 32 9 (Expr (Ecast (Tint I8 Unsigned ) 33 (Expr (Ebinop Odiv 34 (Expr (Ebinop Oadd 35 (Expr (Ecast (Tint I32 Signed ) 36 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 37 (Tint I32 Signed )) 38 (Expr (Ecast (Tint I32 Signed ) 39 (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))) 40 (Tint I32 Signed ))) (Tint I32 Signed )) 41 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 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 ))) 42 20 (Tint I32 Signed ))) (Tint I8 Unsigned ))) 43 21 (Ssequence 44 (Sifthenelse (Expr (Ebinop Oeq 45 (Expr (Ecast (Tint I32 Signed ) 46 (Expr (Ederef 47 (Expr (Ebinop Oadd 48 (Expr (Evar (ident_of_nat 4)) 49 (Tpointer Any (Tint I8 Unsigned ))) 50 (Expr (Evar (ident_of_nat 3)) 51 (Tint I8 Unsigned ))) 52 (Tpointer Any (Tint I8 Unsigned )))) 53 (Tint I8 Unsigned ))) (Tint I32 Signed )) 54 (Expr (Ecast (Tint I32 Signed ) 55 (Expr (Evar (ident_of_nat 6)) (Tint I8 Unsigned ))) 56 (Tint I32 Signed ))) (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)) (Tint I8 Unsigned ))) 73 (Tint I32 Signed ))) (Tint I32 Signed )) 74 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 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 )) 75 31 (Expr (Ecast (Tint I8 Unsigned ) 76 (Expr (Ebinop Osub 77 (Expr (Ecast (Tint I32 Signed ) 78 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))) 79 (Tint I32 Signed )) 80 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 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 ))) 81 41 (Tint I32 Signed ))) (Tint I8 Unsigned ))) 82 Sskip) 83 (Sifthenelse (Expr (Ebinop Olt 84 (Expr (Ecast (Tint I32 Signed ) 85 (Expr (Ederef 86 (Expr (Ebinop Oadd 87 (Expr (Evar (ident_of_nat 4)) 88 (Tpointer Any (Tint I8 Unsigned ))) 89 (Expr (Evar (ident_of_nat 3)) 90 (Tint I8 Unsigned ))) 91 (Tpointer Any (Tint I8 Unsigned )))) 92 (Tint I8 Unsigned ))) (Tint I32 Signed )) 93 (Expr (Ecast (Tint I32 Signed ) 94 (Expr (Evar (ident_of_nat 6)) (Tint I8 Unsigned ))) 95 (Tint I32 Signed ))) (Tint I32 Signed )) 96 (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )) 97 (Expr (Ecast (Tint I8 Unsigned ) 98 (Expr (Ebinop Oadd 99 (Expr (Ecast (Tint I32 Signed ) 100 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))) 101 (Tint I32 Signed )) 102 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 103 (Tint I32 Signed ))) (Tint I8 Unsigned ))) 104 Sskip))))) 105 (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned ) 106 (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1)) 107 (Tint I32 Signed ))) 108 (Tint I32 Signed ))) (Tint I8 Unsigned ))))))) 109 110 111 112 )〉; 113 〈ident_of_nat 7 (* main *), CL_Internal ( 114 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈ident_of_nat 8, (Tint I8 Unsigned )〉 ] 115 (Ssequence 116 (Sassign (Expr (Ederef 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 ) 117 100 (Expr (Ebinop Oadd 118 (Expr (Evar (ident_of_nat 4)) 119 (Tarray Any (Tint I8 Unsigned ) 5)) 120 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 121 (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned )) 122 (Expr (Ecast (Tint I8 Unsigned ) 123 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 124 (Tint I8 Unsigned ))) 125 (Ssequence 126 (Sassign (Expr (Ederef 127 (Expr (Ebinop Oadd 128 (Expr (Evar (ident_of_nat 4)) 129 (Tarray Any (Tint I8 Unsigned ) 5)) 101 (Expr (Ecast (Tint I32 Signed ) 102 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))) 103 (Tint I32 Signed )) 130 104 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 131 (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned )) 132 (Expr (Ecast (Tint I8 Unsigned ) 133 (Expr (Econst_int I32 (repr ? 18)) (Tint I32 Signed ))) 134 (Tint I8 Unsigned ))) 135 (Ssequence 136 (Sassign (Expr (Ederef 137 (Expr (Ebinop Oadd 138 (Expr (Evar (ident_of_nat 4)) 139 (Tarray Any (Tint I8 Unsigned ) 5)) 140 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 141 (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned )) 142 (Expr (Ecast (Tint I8 Unsigned ) 143 (Expr (Econst_int I32 (repr ? 23)) (Tint I32 Signed ))) 144 (Tint I8 Unsigned ))) 145 (Ssequence 146 (Sassign (Expr (Ederef 147 (Expr (Ebinop Oadd 148 (Expr (Evar (ident_of_nat 4)) 149 (Tarray Any (Tint I8 Unsigned ) 5)) 150 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed ))) 151 (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned )) 152 (Expr (Ecast (Tint I8 Unsigned ) 153 (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed ))) 154 (Tint I8 Unsigned ))) 155 (Ssequence 156 (Sassign (Expr (Ederef 157 (Expr (Ebinop Oadd 158 (Expr (Evar (ident_of_nat 4)) 159 (Tarray Any (Tint I8 Unsigned ) 5)) 160 (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed ))) 161 (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned )) 162 (Expr (Ecast (Tint I8 Unsigned ) 163 (Expr (Econst_int I32 (repr ? 120)) (Tint I32 Signed ))) 164 (Tint I8 Unsigned ))) 165 (Ssequence 166 (Scall (Some expr (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned ))) 167 (Expr (Evar (ident_of_nat 0)) 168 (Tfunction (Tcons (Tpointer Any (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I8 Unsigned ))) 169 [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5)); 170 (Expr (Ecast (Tint I8 Unsigned ) 171 (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed ))) 172 (Tint I8 Unsigned )); 173 (Expr (Ecast (Tint I8 Unsigned ) 174 (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed ))) 175 (Tint I8 Unsigned ))]) 176 (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed ) 177 (Expr (Evar (ident_of_nat 8)) 178 (Tint I8 Unsigned ))) (Tint I32 Signed )))))))))) 179 180 181 182 )〉] 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 )〉] 183 185 (ident_of_nat 7) 186 184 187 . 185 188 189 (* 190 example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]). 191 normalize (* you can examine the result here *) 192 *) -
src/Clight/test/sum.c.ma
r1226 r2176 3 3 4 4 definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type) 5 [〈〈ident_of_nat 0 (* src *), Any〉,5 [〈〈ident_of_nat 0 (* src *), XData〉, 6 6 〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ; 7 7 (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ; 8 (Init_int8 (repr I8 4)) ], (Tarray Any(Tint I8 Unsigned ) 5)〉〉]8 (Init_int8 (repr I8 4)) ], (Tarray (Tint I8 Unsigned ) 5)〉〉] 9 9 [〈ident_of_nat 1 (* main *), CL_Internal ( 10 10 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 2, (Tint I32 Signed )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ] … … 21 21 (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed ))) 22 22 (Tint I32 Unsigned)) 23 (Expr (Esizeof (Tarray Any(Tint I8 Unsigned ) 5))23 (Expr (Esizeof (Tarray (Tint I8 Unsigned ) 5)) 24 24 (Tint I32 Unsigned))) (Tint I32 Signed )) 25 25 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed )) … … 38 38 (Expr (Ebinop Oadd 39 39 (Expr (Evar (ident_of_nat 0)) 40 (Tarray Any(Tint I8 Unsigned ) 5))40 (Tarray (Tint I8 Unsigned ) 5)) 41 41 (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed ))) 42 (Tpointer Any (Tint I8 Unsigned ))))43 (Tint I8 Unsigned))) (Tint I32 Signed )))44 (Tint I32 Signed )))(Tint I8 Unsigned )))42 (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))) 43 (Tint I32 Signed ))) (Tint I32 Signed ))) 44 (Tint I8 Unsigned ))) 45 45 ) 46 46 (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed )
Note: See TracChangeset
for help on using the changeset viewer.