| 1 | 
  
    
    | 2 | @type trace | 
  
    
    | 3 | 
  
    
    | 4 | 
 | 
  
    
    | 5 | 
 | 
  
    
    | 6 | 
  
    
    | 7 | 
  
    
    | 8 | 
  
    
    | 9 | 
 | 
  
    
    | 10 | 
  
    
    | 11 | open "f1.txt" [O_TRUNC;O_CREAT;O_WRONLY] 0o666 | 
  
    
    | 12 | Tau | 
  
    
    | 13 | RV_num(3) | 
  
    
    | 14 | write! (FD 3) "0123456789" 10 | 
  
    
    | 15 | Tau | 
  
    
    | 16 | RV_num(10) | 
  
    
    | 17 | close (FD 3) | 
  
    
    | 18 | Tau | 
  
    
    | 19 | RV_none | 
  
    
    | 20 | 
 | 
  
    
    | 21 | open "f1.txt" [O_RDONLY] | 
  
    
    | 22 | Tau | 
  
    
    | 23 | RV_num(3) | 
  
    
    | 24 | 
 | 
  
    
    | 25 | 
  
    
    | 26 | read (FD 3) 2 | 
  
    
    | 27 | Tau | 
  
    
    | 28 | RV_bytes("01") | 
  
    
    | 29 | read (FD 3) 2 | 
  
    
    | 30 | Tau | 
  
    
    | 31 | RV_bytes("23") | 
  
    
    | 32 | 
 | 
  
    
    | 33 | 
  
    
    | 34 | lseek (FD 3) 0 SEEK_SET | 
  
    
    | 35 | Tau | 
  
    
    | 36 | RV_num(0) | 
  
    
    | 37 | read (FD 3) 2 | 
  
    
    | 38 | Tau | 
  
    
    | 39 | RV_bytes("01") | 
  
    
    | 40 | 
 | 
  
    
    | 41 | 
  
    
    | 42 | lseek (FD 3) 4 SEEK_SET | 
  
    
    | 43 | Tau | 
  
    
    | 44 | RV_num(4) | 
  
    
    | 45 | read (FD 3) 2 | 
  
    
    | 46 | Tau | 
  
    
    | 47 | RV_bytes("45") | 
  
    
    | 48 | 
 | 
  
    
    | 49 | 
  
    
    | 50 | lseek (FD 3) 5 SEEK_END | 
  
    
    | 51 | Tau | 
  
    
    | 52 | RV_num(15) | 
  
    
    | 53 | read (FD 3) 2 | 
  
    
    | 54 | Tau | 
  
    
    | 55 | RV_bytes("") | 
  
    
    | 56 | 
 | 
  
    
    | 57 | 
  
    
    | 58 | lseek (FD 3) 5 SEEK_END | 
  
    
    | 59 | Tau | 
  
    
    | 60 | RV_num(15) | 
  
    
    | 61 | read (FD 3) 2 | 
  
    
    | 62 | Tau | 
  
    
    | 63 | RV_bytes("") | 
  
    
    | 64 | 
 | 
  
    
    | 65 | 
  
    
    | 66 | lseek (FD 3) -2 SEEK_END | 
  
    
    | 67 | Tau | 
  
    
    | 68 | RV_num(8) | 
  
    
    | 69 | read (FD 3) 2 | 
  
    
    | 70 | Tau | 
  
    
    | 71 | RV_bytes("89") | 
  
    
    | 72 | 
 | 
  
    
    | 73 | 
  
    
    | 74 | lseek (FD 3) -2 SEEK_CUR | 
  
    
    | 75 | Tau | 
  
    
    | 76 | RV_num(8) | 
  
    
    | 77 | read (FD 3) 2 | 
  
    
    | 78 | Tau | 
  
    
    | 79 | RV_bytes("89") | 
  
    
    | 80 | 
 | 
  
    
    | 81 | 
  
    
    | 82 | lseek (FD 3) -10 SEEK_CUR | 
  
    
    | 83 | Tau | 
  
    
    | 84 | RV_num(0) | 
  
    
    | 85 | read (FD 3) 2 | 
  
    
    | 86 | Tau | 
  
    
    | 87 | RV_bytes("01") | 
  
    
    | 88 | 
 | 
  
    
    | 89 | 
  
    
    | 90 | lseek (FD 3) -10 SEEK_CUR | 
  
    
    | 91 | Tau | 
  
    
    | 92 | EINVAL | 
  
    
    | 93 | read (FD 3) 2 | 
  
    
    | 94 | Tau | 
  
    
    | 95 | RV_bytes("23") | 
  
    
    | 96 | 
 | 
  
    
    | 97 | 
  
    
    | 98 | lseek (FD 3) 0 5 | 
  
    
    | 99 | Tau | 
  
    
    | 100 | EINVAL | 
  
    
    | 101 | read (FD 3) 2 | 
  
    
    | 102 | Tau | 
  
    
    | 103 | RV_bytes("45") | 
  
    
    | 104 | 
 | 
  
    
    | 105 | 
  
    
    | 106 | lseek (FD 3) 0 SEEK_CUR | 
  
    
    | 107 | Tau | 
  
    
    | 108 | RV_num(6) | 
  
    
    | 109 | lseek (FD 3) 0 SEEK_CUR | 
  
    
    | 110 | Tau | 
  
    
    | 111 | RV_num(6) | 
  
    
    | 112 | 
 | 
  
    
    | 113 | close (FD 3) | 
  
    
    | 114 | Tau | 
  
    
    | 115 | RV_none | 
  
    
    | 116 | 
 | 
  
    
    | 117 | 
  
    
    | 118 | lseek (FD 3) 0 SEEK_CUR | 
  
    
    | 119 | Tau | 
  
    
    | 120 | EBADF | 
  
    
    | 121 | 
 | 
  
    
    | 122 | 
  
    
    | 123 | lseek (FD 4) 0 SEEK_CUR | 
  
    
    | 124 | Tau | 
  
    
    | 125 | EBADF | 
  
    
    | 126 | 
 | 
  
    
    | 127 | 
  
    
    | 128 | lseek (FD 4) 0 5 | 
  
    
    | 129 | Tau | 
  
    
    | 130 | EBADF | 
  
    
    | 131 | 
 | 
  
    
    | 132 | 
 | 
  
    
    | 133 | 
  
    
    | 134 | 
  
    
    | 135 | 
  
    
    | 136 | 
 | 
  
    
    | 137 | 
  
    
    | 138 | open "f1.txt" [O_TRUNC;O_WRONLY] 0o666 | 
  
    
    | 139 | Tau | 
  
    
    | 140 | RV_num(3) | 
  
    
    | 141 | lseek (FD 3) 5 SEEK_SET | 
  
    
    | 142 | Tau | 
  
    
    | 143 | RV_num(5) | 
  
    
    | 144 | close (FD 3) | 
  
    
    | 145 | Tau | 
  
    
    | 146 | RV_none | 
  
    
    | 147 | 
 | 
  
    
    | 148 | open "f1.txt" [O_RDONLY] | 
  
    
    | 149 | Tau | 
  
    
    | 150 | RV_num(3) | 
  
    
    | 151 | read! (FD 3) 100 | 
  
    
    | 152 | Tau | 
  
    
    | 153 | RV_bytes("") | 
  
    
    | 154 | close (FD 3) | 
  
    
    | 155 | Tau | 
  
    
    | 156 | RV_none | 
  
    
    | 157 | 
 | 
  
    
    | 158 | 
 | 
  
    
    | 159 | 
  
    
    | 160 | open "f1.txt" [O_TRUNC;O_WRONLY] 0o666 | 
  
    
    | 161 | Tau | 
  
    
    | 162 | RV_num(3) | 
  
    
    | 163 | lseek (FD 3) 5 SEEK_SET | 
  
    
    | 164 | Tau | 
  
    
    | 165 | RV_num(5) | 
  
    
    | 166 | write (FD 3) "0123456789" 10 | 
  
    
    | 167 | Tau | 
  
    
    | 168 | RV_num(10) | 
  
    
    | 169 | close (FD 3) | 
  
    
    | 170 | Tau | 
  
    
    | 171 | RV_none | 
  
    
    | 172 | 
 | 
  
    
    | 173 | open "f1.txt" [O_RDONLY] | 
  
    
    | 174 | Tau | 
  
    
    | 175 | RV_num(3) | 
  
    
    | 176 | read! (FD 3) 100 | 
  
    
    | 177 | Tau | 
  
    
    | 178 | RV_bytes("\000\000\000\000\0000123456789") | 
  
    
    | 179 | close (FD 3) | 
  
    
    | 180 | Tau | 
  
    
    | 181 | RV_none | 
  
    
    | 182 | 
 | 
  
    
    | 183 | 
 | 
  
    
    | 184 | 
  
    
    | 185 | open "f1.txt" [O_TRUNC;O_RDWR] 0o666 | 
  
    
    | 186 | Tau | 
  
    
    | 187 | RV_num(3) | 
  
    
    | 188 | write (FD 3) "0123456789" 10 | 
  
    
    | 189 | Tau | 
  
    
    | 190 | RV_num(10) | 
  
    
    | 191 | lseek (FD 3) -2 SEEK_CUR | 
  
    
    | 192 | Tau | 
  
    
    | 193 | RV_num(8) | 
  
    
    | 194 | write (FD 3) "XX" 2 | 
  
    
    | 195 | Tau | 
  
    
    | 196 | RV_num(2) | 
  
    
    | 197 | lseek (FD 3) -6 SEEK_CUR | 
  
    
    | 198 | Tau | 
  
    
    | 199 | RV_num(4) | 
  
    
    | 200 | read (FD 3) 2 | 
  
    
    | 201 | Tau | 
  
    
    | 202 | RV_bytes("45") | 
  
    
    | 203 | write (FD 3) "YY" 2 | 
  
    
    | 204 | Tau | 
  
    
    | 205 | RV_num(2) | 
  
    
    | 206 | close (FD 3) | 
  
    
    | 207 | Tau | 
  
    
    | 208 | RV_none | 
  
    
    | 209 | 
 | 
  
    
    | 210 | open "f1.txt" [O_RDONLY] | 
  
    
    | 211 | Tau | 
  
    
    | 212 | RV_num(3) | 
  
    
    | 213 | read! (FD 3) 100 | 
  
    
    | 214 | Tau | 
  
    
    | 215 | RV_bytes("012345YYXX") | 
  
    
    | 216 | close (FD 3) | 
  
    
    | 217 | Tau | 
  
    
    | 218 | RV_none | 
  
    
    | 219 | 
 | 
  
    
    | 220 | 
 | 
  
    
    | 221 | 
  
    
    | 222 | 
  
    
    | 223 | 
  
    
    | 224 | 
  
    
    | 225 | 
 | 
  
    
    | 226 | mkdir "d1" 0o777 | 
  
    
    | 227 | Tau | 
  
    
    | 228 | RV_none | 
  
    
    | 229 | open_close "d1/f1.txt" [O_CREAT;O_WRONLY] 0o666 | 
  
    
    | 230 | Tau | 
  
    
    | 231 | RV_none | 
  
    
    | 232 | open_close "d1/f2.txt" [O_CREAT;O_WRONLY] 0o666 | 
  
    
    | 233 | Tau | 
  
    
    | 234 | RV_none | 
  
    
    | 235 | open_close "d1/f3.txt" [O_CREAT;O_WRONLY] 0o666 | 
  
    
    | 236 | Tau | 
  
    
    | 237 | RV_none | 
  
    
    | 238 | 
 | 
  
    
    | 239 | 
 | 
  
    
    | 240 | open "d1" [O_RDONLY] | 
  
    
    | 241 | Tau | 
  
    
    | 242 | RV_num(3) | 
  
    
    | 243 | lseek (FD 3) 0 SEEK_CUR | 
  
    
    | 244 | Tau | 
  
    
    | 245 | RV_num(0) | 
  
    
    | 246 | read (FD 3) 10 | 
  
    
    | 247 | Tau | 
  
    
    | 248 | EISDIR | 
  
    
    | 249 | 
 | 
  
    
    | 250 | lseek (FD 3) 4 SEEK_CUR | 
  
    
    | 251 | Tau | 
  
    
    | 252 | RV_num(4) | 
  
    
    | 253 | read (FD 3) 10 | 
  
    
    | 254 | Tau | 
  
    
    | 255 | EISDIR | 
  
    
    | 256 | 
 | 
  
    
    | 257 | 
  
    
    | 258 | lseek (FD 3) 0 SEEK_END | 
  
    
    | 259 | Tau | 
  
    
    
    | 260 | RV_num(0) | 
  
    |  | 
      | THE SPEC ASSERTS THE STATE SET IS EMPTY |  | The spec permitted: |  | expected error EOVERFLOW but got value RV_num(0) |  | 
  
    
    | 261 | lseek (FD 3) -2000 SEEK_END | 
  
    
    | 262 | Tau | 
  
    
    
    | 263 | EINVAL | 
  
    |  | 
      | THE SPEC ASSERTS THE STATE SET IS EMPTY |  | The spec permitted: |  | expected error EOVERFLOW but got error EINVAL |  | 
  
    
    | 264 | 
 | 
  
    
    | 265 | lseek (FD 3) 0 SEEK_SET | 
  
    
    | 266 | Tau | 
  
    
    | 267 | RV_num(0) | 
  
    
    | 268 | read (FD 3) 10 | 
  
    
    | 269 | Tau | 
  
    
    | 270 | EISDIR | 
  
    
    | 271 | 
 | 
  
    
    | 272 | lseek (FD 3) 10 SEEK_SET | 
  
    
    | 273 | Tau | 
  
    
    | 274 | RV_num(10) | 
  
    
    | 275 | read (FD 3) 10 | 
  
    
    | 276 | Tau | 
  
    
    | 277 | EISDIR | 
  
    
    | 278 | 
 | 
  
    
    | 279 | close (FD 3) | 
  
    
    | 280 | Tau | 
  
    
    | 281 | RV_none | 
  
    
    | 282 | 
 | 
  
    
    | 283 | 
 |