| 1 | 
  
    
    | 2 | @type trace | 
  
    
    | 3 | 
  
    
    | 4 | 
 | 
  
    
    | 5 | 
 | 
  
    
    | 6 | 
  
    
    | 7 | 
  
    
    | 8 | 
  
    
    | 9 | 
 | 
  
    
    | 10 | 
  
    
    | 11 | mkdir "/empty_dir" 0o777 | 
  
    
    | 12 | Tau | 
  
    
    | 13 | RV_none | 
  
    
    | 14 | mkdir "/non_empty_dir" 0o777 | 
  
    
    | 15 | Tau | 
  
    
    | 16 | RV_none | 
  
    
    | 17 | 
 | 
  
    
    | 18 | chdir "/non_empty_dir" | 
  
    
    | 19 | Tau | 
  
    
    | 20 | RV_none | 
  
    
    | 21 | 
 | 
  
    
    | 22 | 
 | 
  
    
    | 23 | 
  
    
    | 24 | 
  
    
    | 25 | 
  
    
    | 26 | 
 | 
  
    
    | 27 | 
  
    
    | 28 | open "f1.txt" [O_CREAT;O_RDWR] 0o666 | 
  
    
    | 29 | Tau | 
  
    
    | 30 | RV_num(3) | 
  
    
    | 31 | write (FD 3) "0123456789" 10 | 
  
    
    | 32 | Tau | 
  
    
    | 33 | RV_num(10) | 
  
    
    | 34 | close (FD 3) | 
  
    
    | 35 | Tau | 
  
    
    | 36 | RV_none | 
  
    
    | 37 | 
 | 
  
    
    | 38 | open "f1.txt" [O_RDONLY] | 
  
    
    | 39 | Tau | 
  
    
    | 40 | RV_num(3) | 
  
    
    | 41 | read! (FD 3) 100 | 
  
    
    | 42 | Tau | 
  
    
    | 43 | RV_bytes("0123456789") | 
  
    
    | 44 | close (FD 3) | 
  
    
    | 45 | Tau | 
  
    
    | 46 | RV_none | 
  
    
    | 47 | 
 | 
  
    
    | 48 | 
  
    
    | 49 | open "f1.txt" [O_APPEND;O_RDWR] 0o666 | 
  
    
    | 50 | Tau | 
  
    
    | 51 | RV_num(3) | 
  
    
    | 52 | write (FD 3) "0123456789" 10 | 
  
    
    | 53 | Tau | 
  
    
    | 54 | RV_num(10) | 
  
    
    | 55 | close (FD 3) | 
  
    
    | 56 | Tau | 
  
    
    | 57 | RV_none | 
  
    
    | 58 | 
 | 
  
    
    | 59 | open "f1.txt" [O_RDONLY] | 
  
    
    | 60 | Tau | 
  
    
    | 61 | RV_num(3) | 
  
    
    | 62 | read! (FD 3) 100 | 
  
    
    | 63 | Tau | 
  
    
    | 64 | RV_bytes("01234567890123456789") | 
  
    
    | 65 | close (FD 3) | 
  
    
    | 66 | Tau | 
  
    
    | 67 | RV_none | 
  
    
    | 68 | 
 | 
  
    
    | 69 | 
  
    
    | 70 | open "f1.txt" [O_RDWR] 0o666 | 
  
    
    | 71 | Tau | 
  
    
    | 72 | RV_num(3) | 
  
    
    | 73 | write (FD 3) "XXX" 3 | 
  
    
    | 74 | Tau | 
  
    
    | 75 | RV_num(3) | 
  
    
    | 76 | close (FD 3) | 
  
    
    | 77 | Tau | 
  
    
    | 78 | RV_none | 
  
    
    | 79 | 
 | 
  
    
    | 80 | open "f1.txt" [O_RDONLY] | 
  
    
    | 81 | Tau | 
  
    
    | 82 | RV_num(3) | 
  
    
    | 83 | read! (FD 3) 100 | 
  
    
    | 84 | Tau | 
  
    
    | 85 | RV_bytes("XXX34567890123456789") | 
  
    
    | 86 | close (FD 3) | 
  
    
    | 87 | Tau | 
  
    
    | 88 | RV_none | 
  
    
    | 89 | 
 | 
  
    
    | 90 | 
  
    
    | 91 | open "f1.txt" [O_TRUNC;O_RDWR] 0o666 | 
  
    
    | 92 | Tau | 
  
    
    | 93 | RV_num(3) | 
  
    
    | 94 | write (FD 3) "0123456789" 10 | 
  
    
    | 95 | Tau | 
  
    
    | 96 | RV_num(10) | 
  
    
    | 97 | close (FD 3) | 
  
    
    | 98 | Tau | 
  
    
    | 99 | RV_none | 
  
    
    | 100 | 
 | 
  
    
    | 101 | open "f1.txt" [O_RDONLY] | 
  
    
    | 102 | Tau | 
  
    
    | 103 | RV_num(3) | 
  
    
    | 104 | read! (FD 3) 100 | 
  
    
    | 105 | Tau | 
  
    
    | 106 | RV_bytes("0123456789") | 
  
    
    | 107 | close (FD 3) | 
  
    
    | 108 | Tau | 
  
    
    | 109 | RV_none | 
  
    
    | 110 | 
 | 
  
    
    | 111 | 
  
    
    | 112 | open "f1.txt" [O_TRUNC;O_RDWR] 0o666 | 
  
    
    | 113 | Tau | 
  
    
    | 114 | RV_num(3) | 
  
    
    | 115 | write (FD 3) "0123456789" 5 | 
  
    
    | 116 | Tau | 
  
    
    | 117 | RV_num(5) | 
  
    
    | 118 | close (FD 3) | 
  
    
    | 119 | Tau | 
  
    
    | 120 | RV_none | 
  
    
    | 121 | 
 | 
  
    
    | 122 | open "f1.txt" [O_RDONLY] | 
  
    
    | 123 | Tau | 
  
    
    | 124 | RV_num(3) | 
  
    
    | 125 | read! (FD 3) 100 | 
  
    
    | 126 | Tau | 
  
    
    | 127 | RV_bytes("01234") | 
  
    
    | 128 | close (FD 3) | 
  
    
    | 129 | Tau | 
  
    
    | 130 | RV_none | 
  
    
    | 131 | 
 | 
  
    
    | 132 | 
  
    
    | 133 | open "f1.txt" [O_RDWR] | 
  
    
    | 134 | Tau | 
  
    
    | 135 | RV_num(3) | 
  
    
    | 136 | write (FD 3) "9876543210" 0 | 
  
    
    | 137 | Tau | 
  
    
    | 138 | RV_num(0) | 
  
    
    | 139 | close (FD 3) | 
  
    
    | 140 | Tau | 
  
    
    | 141 | RV_none | 
  
    
    | 142 | 
 | 
  
    
    | 143 | open "f1.txt" [O_RDONLY] | 
  
    
    | 144 | Tau | 
  
    
    | 145 | RV_num(3) | 
  
    
    | 146 | read! (FD 3) 100 | 
  
    
    | 147 | Tau | 
  
    
    | 148 | RV_bytes("01234") | 
  
    
    | 149 | close (FD 3) | 
  
    
    | 150 | Tau | 
  
    
    | 151 | RV_none | 
  
    
    | 152 | 
 | 
  
    
    | 153 | 
  
    
    | 154 | 
  
    
    | 155 | 
  
    
    | 156 | 
 | 
  
    
    | 157 | 
  
    
    | 158 | open "f1.txt" [O_TRUNC;O_RDWR] 0o666 | 
  
    
    | 159 | Tau | 
  
    
    | 160 | RV_num(3) | 
  
    
    | 161 | write (FD 3) "0123456789" 10 | 
  
    
    | 162 | Tau | 
  
    
    | 163 | RV_num(10) | 
  
    
    | 164 | pwrite (FD 3) "X" 1 4 | 
  
    
    | 165 | Tau | 
  
    
    | 166 | RV_num(1) | 
  
    
    | 167 | pwrite (FD 3) "X" 1 6 | 
  
    
    | 168 | Tau | 
  
    
    | 169 | RV_num(1) | 
  
    
    | 170 | pwrite (FD 3) "X" 1 8 | 
  
    
    | 171 | Tau | 
  
    
    | 172 | RV_num(1) | 
  
    
    | 173 | write (FD 3) "0123456789" 10 | 
  
    
    | 174 | Tau | 
  
    
    | 175 | RV_num(10) | 
  
    
    | 176 | close (FD 3) | 
  
    
    | 177 | Tau | 
  
    
    | 178 | RV_none | 
  
    
    | 179 | 
 | 
  
    
    | 180 | open "f1.txt" [O_RDONLY] | 
  
    
    | 181 | Tau | 
  
    
    | 182 | RV_num(3) | 
  
    
    | 183 | read! (FD 3) 100 | 
  
    
    | 184 | Tau | 
  
    
    | 185 | RV_bytes("0123X5X7X90123456789") | 
  
    
    | 186 | close (FD 3) | 
  
    
    | 187 | Tau | 
  
    
    | 188 | RV_none | 
  
    
    | 189 | 
 | 
  
    
    | 190 | 
 | 
  
    
    | 191 | 
  
    
    | 192 | open "f1.txt" [O_TRUNC;O_RDWR] 0o666 | 
  
    
    | 193 | Tau | 
  
    
    | 194 | RV_num(3) | 
  
    
    | 195 | pwrite (FD 3) "XXX" 3 10 | 
  
    
    | 196 | Tau | 
  
    
    | 197 | RV_num(3) | 
  
    
    | 198 | close (FD 3) | 
  
    
    | 199 | Tau | 
  
    
    | 200 | RV_none | 
  
    
    | 201 | 
 | 
  
    
    | 202 | open "f1.txt" [O_RDONLY] | 
  
    
    | 203 | Tau | 
  
    
    | 204 | RV_num(3) | 
  
    
    | 205 | read! (FD 3) 100 | 
  
    
    | 206 | Tau | 
  
    
    | 207 | RV_bytes("\000\000\000\000\000\000\000\000\000\000XXX") | 
  
    
    | 208 | close (FD 3) | 
  
    
    | 209 | Tau | 
  
    
    | 210 | RV_none | 
  
    
    | 211 | 
 | 
  
    
    | 212 | 
 | 
  
    
    | 213 | 
  
    
    | 214 | open "f1.txt" [O_TRUNC;O_RDWR] 0o666 | 
  
    
    | 215 | Tau | 
  
    
    | 216 | RV_num(3) | 
  
    
    | 217 | pwrite (FD 3) "XXX" 3 10 | 
  
    
    | 218 | Tau | 
  
    
    | 219 | RV_num(3) | 
  
    
    | 220 | write (FD 3) "01234" 5 | 
  
    
    | 221 | Tau | 
  
    
    | 222 | RV_num(5) | 
  
    
    | 223 | close (FD 3) | 
  
    
    | 224 | Tau | 
  
    
    | 225 | RV_none | 
  
    
    | 226 | 
 | 
  
    
    | 227 | open "f1.txt" [O_RDONLY] | 
  
    
    | 228 | Tau | 
  
    
    | 229 | RV_num(3) | 
  
    
    | 230 | read! (FD 3) 100 | 
  
    
    | 231 | Tau | 
  
    
    | 232 | RV_bytes("01234\000\000\000\000\000XXX") | 
  
    
    | 233 | close (FD 3) | 
  
    
    | 234 | Tau | 
  
    
    | 235 | RV_none | 
  
    
    | 236 | 
 | 
  
    
    | 237 | 
 | 
  
    
    | 238 | 
 | 
  
    
    | 239 | 
  
    
    | 240 | 
  
    
    | 241 | 
  
    
    | 242 | 
 | 
  
    
    | 243 | open "f1.txt" [O_TRUNC;O_RDWR] 0o666 | 
  
    
    | 244 | Tau | 
  
    
    | 245 | RV_num(3) | 
  
    
    | 246 | write (FD 3) "0123456789" 10 | 
  
    
    | 247 | Tau | 
  
    
    | 248 | RV_num(10) | 
  
    
    | 249 | lseek (FD 3) -3 SEEK_CUR | 
  
    
    | 250 | Tau | 
  
    
    | 251 | RV_num(7) | 
  
    
    | 252 | write (FD 3) "ABC" 3 | 
  
    
    | 253 | Tau | 
  
    
    | 254 | RV_num(3) | 
  
    
    | 255 | pwrite (FD 3) "X" 1 4 | 
  
    
    | 256 | Tau | 
  
    
    | 257 | RV_num(1) | 
  
    
    | 258 | lseek (FD 3) 2 SEEK_SET | 
  
    
    | 259 | Tau | 
  
    
    | 260 | RV_num(2) | 
  
    
    | 261 | write (FD 3) "Y" 1 | 
  
    
    | 262 | Tau | 
  
    
    | 263 | RV_num(1) | 
  
    
    | 264 | lseek (FD 3) 0 SEEK_SET | 
  
    
    | 265 | Tau | 
  
    
    | 266 | RV_num(0) | 
  
    
    | 267 | read! (FD 3) 100 | 
  
    
    | 268 | Tau | 
  
    
    | 269 | RV_bytes("01Y3X56ABC") | 
  
    
    | 270 | close (FD 3) | 
  
    
    | 271 | Tau | 
  
    
    | 272 | RV_none | 
  
    
    | 273 | 
 | 
  
    
    | 274 | 
  
    
    | 275 | open "f1.txt" [O_TRUNC;O_RDWR] 0o666 | 
  
    
    | 276 | Tau | 
  
    
    | 277 | RV_num(3) | 
  
    
    | 278 | write (FD 3) "0123456789" 10 | 
  
    
    | 279 | Tau | 
  
    
    | 280 | RV_num(10) | 
  
    
    | 281 | lseek (FD 3) 5 SEEK_CUR | 
  
    
    | 282 | Tau | 
  
    
    | 283 | RV_num(15) | 
  
    
    | 284 | write (FD 3) "ABCDE" 5 | 
  
    
    | 285 | Tau | 
  
    
    | 286 | RV_num(5) | 
  
    
    | 287 | lseek (FD 3) 0 SEEK_SET | 
  
    
    | 288 | Tau | 
  
    
    | 289 | RV_num(0) | 
  
    
    | 290 | read! (FD 3) 100 | 
  
    
    | 291 | Tau | 
  
    
    | 292 | RV_bytes("0123456789\000\000\000\000\000ABCDE") | 
  
    
    | 293 | close (FD 3) | 
  
    
    | 294 | Tau | 
  
    
    | 295 | RV_none | 
  
    
    | 296 | 
 | 
  
    
    | 297 | 
  
    
    | 298 | 
  
    
    | 299 | 
  
    
    | 300 | 
 | 
  
    
    | 301 | 
  
    
    | 302 | open "f1.txt" [O_TRUNC;O_RDWR] | 
  
    
    | 303 | Tau | 
  
    
    | 304 | RV_num(3) | 
  
    
    | 305 | write (FD 3) "0123456789" 10 | 
  
    
    | 306 | Tau | 
  
    
    | 307 | RV_num(10) | 
  
    
    | 308 | lseek (FD 3) 0 SEEK_SET | 
  
    
    | 309 | Tau | 
  
    
    | 310 | RV_num(0) | 
  
    
    | 311 | read! (FD 3) 100 | 
  
    
    | 312 | Tau | 
  
    
    | 313 | RV_bytes("0123456789") | 
  
    
    | 314 | close (FD 3) | 
  
    
    | 315 | Tau | 
  
    
    | 316 | RV_none | 
  
    
    | 317 | 
 | 
  
    
    | 318 | 
  
    
    | 319 | open "f1.txt" [O_TRUNC;O_WRONLY] | 
  
    
    | 320 | Tau | 
  
    
    | 321 | RV_num(3) | 
  
    
    | 322 | write (FD 3) "ABCDE" 5 | 
  
    
    | 323 | Tau | 
  
    
    | 324 | RV_num(5) | 
  
    
    | 325 | close (FD 3) | 
  
    
    | 326 | Tau | 
  
    
    | 327 | RV_none | 
  
    
    | 328 | open "f1.txt" [O_RDONLY] | 
  
    
    | 329 | Tau | 
  
    
    | 330 | RV_num(3) | 
  
    
    | 331 | read! (FD 3) 100 | 
  
    
    | 332 | Tau | 
  
    
    | 333 | RV_bytes("ABCDE") | 
  
    
    | 334 | close (FD 3) | 
  
    
    | 335 | Tau | 
  
    
    | 336 | RV_none | 
  
    
    | 337 | 
 | 
  
    
    | 338 | 
  
    
    | 339 | open "f1.txt" [O_WRONLY] | 
  
    
    | 340 | Tau | 
  
    
    | 341 | RV_num(3) | 
  
    
    | 342 | write (FD 3) "012" 3 | 
  
    
    | 343 | Tau | 
  
    
    | 344 | RV_num(3) | 
  
    
    | 345 | lseek (FD 3) 0 SEEK_SET | 
  
    
    | 346 | Tau | 
  
    
    | 347 | RV_num(0) | 
  
    
    | 348 | read (FD 3) 100 | 
  
    
    | 349 | Tau | 
  
    
    | 350 | EBADF | 
  
    
    | 351 | close (FD 3) | 
  
    
    | 352 | Tau | 
  
    
    | 353 | RV_none | 
  
    
    | 354 | 
 | 
  
    
    | 355 | open "f1.txt" [O_RDONLY] | 
  
    
    | 356 | Tau | 
  
    
    | 357 | RV_num(3) | 
  
    
    | 358 | read! (FD 3) 100 | 
  
    
    | 359 | Tau | 
  
    
    | 360 | RV_bytes("012DE") | 
  
    
    | 361 | close (FD 3) | 
  
    
    | 362 | Tau | 
  
    
    | 363 | RV_none | 
  
    
    | 364 | 
 | 
  
    
    | 365 | 
  
    
    | 366 | open "f1.txt" [O_APPEND;O_RDWR] | 
  
    
    | 367 | Tau | 
  
    
    | 368 | RV_num(3) | 
  
    
    | 369 | write (FD 3) "ABCDE" 5 | 
  
    
    | 370 | Tau | 
  
    
    | 371 | RV_num(5) | 
  
    
    | 372 | lseek (FD 3) 0 SEEK_SET | 
  
    
    | 373 | Tau | 
  
    
    | 374 | RV_num(0) | 
  
    
    | 375 | read! (FD 3) 100 | 
  
    
    | 376 | Tau | 
  
    
    | 377 | RV_bytes("012DEABCDE") | 
  
    
    | 378 | close (FD 3) | 
  
    
    | 379 | Tau | 
  
    
    | 380 | RV_none | 
  
    
    | 381 | 
 | 
  
    
    | 382 | 
  
    
    | 383 | open "f1.txt" [O_RDONLY] | 
  
    
    | 384 | Tau | 
  
    
    | 385 | RV_num(3) | 
  
    
    | 386 | write (FD 3) "ABCDE" 5 | 
  
    
    | 387 | Tau | 
  
    
    | 388 | EBADF | 
  
    
    | 389 | lseek (FD 3) 0 SEEK_SET | 
  
    
    | 390 | Tau | 
  
    
    | 391 | RV_num(0) | 
  
    
    | 392 | read (FD 3) 100 | 
  
    
    | 393 | Tau | 
  
    
    | 394 | RV_bytes("012DEABCDE") | 
  
    
    | 395 | close (FD 3) | 
  
    
    | 396 | Tau | 
  
    
    | 397 | RV_none | 
  
    
    | 398 | 
 | 
  
    
    | 399 | 
  
    
    | 400 | write (FD 3) "ABCDE" 5 | 
  
    
    | 401 | Tau | 
  
    
    | 402 | EBADF | 
  
    
    | 403 | 
 | 
  
    
    | 404 | 
  
    
    | 405 | write (FD 300) "ABCDE" 5 | 
  
    
    | 406 | Tau | 
  
    
    | 407 | EBADF | 
  
    
    | 408 | 
 | 
  
    
    | 409 | 
 | 
  
    
    | 410 | 
  
    
    | 411 | 
  
    
    | 412 | 
  
    
    | 413 | 
  
    
    | 414 | 
  
    
    | 415 | 
 | 
  
    
    | 416 | open "/non_empty_dir" [O_RDWR] | 
  
    
    | 417 | Tau | 
  
    
    | 418 | EISDIR | 
  
    
    | 419 | write (FD 3) "ABC" 3 | 
  
    
    | 420 | Tau | 
  
    
    | 421 | EBADF | 
  
    
    | 422 | close (FD 3) | 
  
    
    | 423 | Tau | 
  
    
    | 424 | EBADF | 
  
    
    | 425 | 
 | 
  
    
    | 426 | open "/non_empty_dir" [O_RDWR] | 
  
    
    | 427 | Tau | 
  
    
    | 428 | EISDIR | 
  
    
    | 429 | 
  
    
    | 430 | write (FD 3) "ABC" 0 | 
  
    
    | 431 | Tau | 
  
    
    
    | 432 | RV_num(0) | 
  
    |  | 
      | THE SPEC ASSERTS THE STATE SET IS EMPTY |  | The spec permitted: |  | expected error EBADF but got value RV_num(0) |  | 
  
    
    | 433 | close (FD 3) | 
  
    
    | 434 | Tau | 
  
    
    | 435 | EBADF | 
  
    
    | 436 | 
 | 
  
    
    | 437 | open "/non_empty_dir" [O_WRONLY] | 
  
    
    | 438 | Tau | 
  
    
    | 439 | EISDIR | 
  
    
    | 440 | write (FD 3) "ABC" 3 | 
  
    
    | 441 | Tau | 
  
    
    | 442 | EBADF | 
  
    
    | 443 | close (FD 3) | 
  
    
    | 444 | Tau | 
  
    
    | 445 | EBADF | 
  
    
    | 446 | 
 | 
  
    
    | 447 | open "/non_empty_dir" [O_RDONLY] | 
  
    
    | 448 | Tau | 
  
    
    | 449 | RV_num(3) | 
  
    
    | 450 | write (FD 3) "ABC" 0 | 
  
    
    | 451 | Tau | 
  
    
    
    | 452 | RV_num(0) | 
  
    |  | 
      | THE SPEC ASSERTS THE STATE SET IS EMPTY |  | The spec permitted: |  | expected error EBADF but got value RV_num(0) |  | 
  
    
    | 453 | write (FD 3) "ABC" 3 | 
  
    
    | 454 | Tau | 
  
    
    | 455 | EBADF | 
  
    
    | 456 | close (FD 3) | 
  
    
    | 457 | Tau | 
  
    
    | 458 | RV_none | 
  
    
    | 459 | 
 | 
  
    
    | 460 | 
  
    
    | 461 | 
  
    
    | 462 | 
  
    
    | 463 | symlink "/non_empty_dir/target" "/non_empty_dir/symlink" | 
  
    
    | 464 | Tau | 
  
    
    | 465 | RV_none | 
  
    
    | 466 | 
 | 
  
    
    | 467 | open "/non_empty_dir/symlink" [O_WRONLY] | 
  
    
    | 468 | Tau | 
  
    
    | 469 | ENOENT | 
  
    
    | 470 | write (FD 3) "ABC" 1 | 
  
    
    | 471 | Tau | 
  
    
    | 472 | EBADF | 
  
    
    | 473 | close (FD 3) | 
  
    
    | 474 | Tau | 
  
    
    | 475 | EBADF | 
  
    
    | 476 | 
 | 
  
    
    | 477 | readlink "/non_empty_dir/symlink" | 
  
    
    | 478 | Tau | 
  
    
    | 479 | RV_bytes("/non_empty_dir/target") | 
  
    
    | 480 | 
 | 
  
    
    | 481 | open "/non_empty_dir/symlink" [O_WRONLY] | 
  
    
    | 482 | Tau | 
  
    
    | 483 | ENOENT | 
  
    
    | 484 | 
  
    
    | 485 | write (FD 3) "" 0 | 
  
    
    | 486 | Tau | 
  
    
    
    | 487 | RV_num(0) | 
  
    |  | 
      | THE SPEC ASSERTS THE STATE SET IS EMPTY |  | The spec permitted: |  | expected error EBADF but got value RV_num(0) |  | 
  
    
    | 488 | close (FD 3) | 
  
    
    | 489 | Tau | 
  
    
    | 490 | EBADF | 
  
    
    | 491 | 
 | 
  
    
    | 492 | readlink "/non_empty_dir/symlink" | 
  
    
    | 493 | Tau | 
  
    
    | 494 | RV_bytes("/non_empty_dir/target") | 
  
    
    | 495 | 
 | 
  
    
    | 496 | 
  
    
    | 497 | 
  
    
    | 498 | 
  
    
    | 499 | 
 | 
  
    
    | 500 | open "/file1" [O_CREAT;O_RDWR] 0o666 | 
  
    
    | 501 | Tau | 
  
    
    | 502 | RV_num(3) | 
  
    
    | 503 | pwrite! (FD 3) "ABC" 3 0 | 
  
    
    | 504 | Tau | 
  
    
    | 505 | RV_num(3) | 
  
    
    | 506 | close (FD 3) | 
  
    
    | 507 | Tau | 
  
    
    | 508 | RV_none | 
  
    
    | 509 | 
 | 
  
    
    | 510 | open "/file1" [O_APPEND;O_RDWR] | 
  
    
    | 511 | Tau | 
  
    
    | 512 | RV_num(3) | 
  
    
    | 513 | pwrite! (FD 3) "ABCDF" 5 0 | 
  
    
    | 514 | Tau | 
  
    
    | 515 | RV_num(5) | 
  
    
    | 516 | close (FD 3) | 
  
    
    | 517 | Tau | 
  
    
    | 518 | RV_none | 
  
    
    | 519 | 
 | 
  
    
    | 520 | 
 | 
  
    
    | 521 | 
 | 
  
    
    | 522 | 
  
    
    | 523 | 
  
    
    | 524 | 
  
    
    | 525 | 
 | 
  
    
    | 526 | write (FD 99) "" 0 | 
  
    
    | 527 | Tau | 
  
    
    
    | 528 | RV_num(0) | 
  
    |  | 
      | THE SPEC ASSERTS THE STATE SET IS EMPTY |  | The spec permitted: |  | expected error EBADF but got value RV_num(0) |  | 
  
    
    | 529 | 
 | 
  
    
    | 530 | 
 |