| 1 |
| 2 |
@type trace |
| 3 |
| 4 |
|
| 5 |
Pid 2 -> create (User_id 1) (Group_id 1) |
| 6 |
|
| 7 |
Pid 2 -> symlink "b" "a" |
| 8 |
Tau |
| 9 |
RV_none |
| 10 |
|
| 11 |
lstat "a" |
| 12 |
Tau |
| 13 |
RV_stat {
| st_dev | = | 1792; |
| st_ino | = |
13; |
| st_kind | = |
S_IFLNK; |
| st_perm | = |
0o777; |
| st_nlink | = | 1; |
| st_uid | = |
1; |
| st_gid | = |
1; |
| st_rdev | = | 0; |
| st_size | = |
1; |
} |
|
| THE SPEC ASSERTS THE STATE SET IS EMPTY |
The spec permitted:
RV_stat {
| st_dev | = | 2049; |
| st_ino | = |
1; |
| st_kind | = |
S_IFLNK; |
| st_perm | = |
0o777; |
| st_nlink | = | 1; |
| st_uid | = |
0; |
| st_gid | = |
0; |
| st_rdev | = | 0; |
| st_size | = |
1; |
}
|
| expected st_uid 0 but got st_uid 1expected st_gid 0 but got st_gid 1 |
|
| 14 |
|
| 15 |
Pid 2 -> mkdir "d" 0o777 |
| 16 |
Tau |
| 17 |
RV_none |
| 18 |
|
| 19 |
stat "d" |
| 20 |
Tau |
| 21 |
RV_stat {
| st_dev | = | 1792; |
| st_ino | = |
32646; |
| st_kind | = |
S_IFDIR; |
| st_perm | = |
0o755; |
| st_nlink | = | 2; |
| st_uid | = |
1; |
| st_gid | = |
1; |
| st_rdev | = | 0; |
| st_size | = |
4096; |
} |
| 22 |
|
| 23 |
Pid 2 -> open_close "c" [O_CREAT;O_RDWR] 0o666 |
| 24 |
Tau |
| 25 |
RV_none |
| 26 |
|
| 27 |
stat "c" |
| 28 |
Tau |
| 29 |
RV_stat {
| st_dev | = | 1792; |
| st_ino | = |
14; |
| st_kind | = |
S_IFREG; |
| st_perm | = |
0o644; |
| st_nlink | = | 1; |
| st_uid | = |
1; |
| st_gid | = |
1; |
| st_rdev | = | 0; |
| st_size | = |
0; |
} |
| 30 |
|
| 31 |
|