| 1 | 
  
    
    | 2 | @type trace | 
  
    
    | 3 | 
 | 
  
    
    | 4 | 
  
    
    | 5 | 
  
    
    | 6 | 
  
    
    | 7 | 
 | 
  
    
    | 8 | 
  
    
    | 9 | 
 | 
  
    
    | 10 | open_close "/f1.txt" [O_RDONLY;O_CREAT] 0o666 | 
  
    
    | 11 | Tau | 
  
    
    | 12 | RV_none | 
  
    
    | 13 | 
 | 
  
    
    | 14 | link "/f1.txt" "/f1_hl.txt" | 
  
    
    | 15 | Tau | 
  
    
    | 16 | RV_none | 
  
    
    | 17 | 
 | 
  
    
    | 18 | stat "f1.txt" | 
  
    
    | 19 | Tau | 
  
    
    | 20 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 295281; |  | st_kind | = | S_IFREG; |  | st_perm | = | 0o644; |  | st_nlink | = | 2; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 0; |  } | 
  
    
    | 21 | 
 | 
  
    
    | 22 | stat "f1_hl.txt" | 
  
    
    | 23 | Tau | 
  
    
    | 24 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 295282; |  | st_kind | = | S_IFREG; |  | st_perm | = | 0o644; |  | st_nlink | = | 2; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 0; |  } | 
  
    
    | 25 | 
 | 
  
    
    | 26 | rename "f1.txt" "f2.txt" | 
  
    
    | 27 | Tau | 
  
    
    | 28 | RV_none | 
  
    
    | 29 | 
 | 
  
    
    | 30 | stat "f2.txt" | 
  
    
    | 31 | Tau | 
  
    
    | 32 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 295281; |  | st_kind | = | S_IFREG; |  | st_perm | = | 0o644; |  | st_nlink | = | 2; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 0; |  } | 
  
    
    | 33 | 
 | 
  
    
    | 34 | stat "f1_hl.txt" | 
  
    
    | 35 | Tau | 
  
    
    | 36 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 295282; |  | st_kind | = | S_IFREG; |  | st_perm | = | 0o644; |  | st_nlink | = | 2; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 0; |  } | 
  
    
    | 37 | 
 | 
  
    
    | 38 | 
  
    
    | 39 | 
 | 
  
    
    | 40 | mkdir "/nonempty_dir1" 0o777 | 
  
    
    | 41 | Tau | 
  
    
    | 42 | RV_none | 
  
    
    | 43 | 
 | 
  
    
    | 44 | stat "/nonempty_dir1" | 
  
    
    | 45 | Tau | 
  
    
    
    | 46 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 295288; |  | st_kind | = | S_IFDIR; |  | st_perm | = | 0o755; |  | st_nlink | = | 1; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 0; |  } | 
  
    |  | 
      | THE SPEC ASSERTS THE STATE SET IS EMPTY |  | The spec permitted: RV_stat { 
      | st_dev | = | 2049; |  | st_ino | = | 2; |  | st_kind | = | S_IFDIR; |  | st_perm | = | 0o755; |  | st_nlink | = | 2; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 9999; |  }
 |  | expected st_nlink 2 but got st_nlink 1 |  | 
  
    
    | 47 | 
 | 
  
    
    | 48 | mkdir "/nonempty_dir2" 0o777 | 
  
    
    | 49 | Tau | 
  
    
    | 50 | RV_none | 
  
    
    | 51 | 
 | 
  
    
    | 52 | stat "/nonempty_dir2" | 
  
    
    | 53 | Tau | 
  
    
    
    | 54 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 295290; |  | st_kind | = | S_IFDIR; |  | st_perm | = | 0o755; |  | st_nlink | = | 1; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 0; |  } | 
  
    |  | 
      | THE SPEC ASSERTS THE STATE SET IS EMPTY |  | The spec permitted: RV_stat { 
      | st_dev | = | 2049; |  | st_ino | = | 3; |  | st_kind | = | S_IFDIR; |  | st_perm | = | 0o755; |  | st_nlink | = | 2; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 9999; |  }
 |  | expected st_nlink 2 but got st_nlink 1 |  | 
  
    
    | 55 | 
 | 
  
    
    | 56 | mkdir "/nonempty_dir1/mydir" 0o777 | 
  
    
    | 57 | Tau | 
  
    
    | 58 | RV_none | 
  
    
    | 59 | 
 | 
  
    
    | 60 | stat "/nonempty_dir1/mydir" | 
  
    
    | 61 | Tau | 
  
    
    
    | 62 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 295293; |  | st_kind | = | S_IFDIR; |  | st_perm | = | 0o755; |  | st_nlink | = | 1; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 0; |  } | 
  
    |  | 
      | THE SPEC ASSERTS THE STATE SET IS EMPTY |  | The spec permitted: RV_stat { 
      | st_dev | = | 2049; |  | st_ino | = | 4; |  | st_kind | = | S_IFDIR; |  | st_perm | = | 0o755; |  | st_nlink | = | 2; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 9999; |  }
 |  | expected st_nlink 2 but got st_nlink 1 |  | 
  
    
    | 63 | 
 | 
  
    
    | 64 | rename "/nonempty_dir1/mydir" "/nonempty_dir2/mydir" | 
  
    
    | 65 | Tau | 
  
    
    | 66 | RV_none | 
  
    
    | 67 | 
 | 
  
    
    | 68 | stat "/nonempty_dir1" | 
  
    
    | 69 | Tau | 
  
    
    
    | 70 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 295288; |  | st_kind | = | S_IFDIR; |  | st_perm | = | 0o755; |  | st_nlink | = | 1; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 0; |  } | 
  
    |  | 
      | THE SPEC ASSERTS THE STATE SET IS EMPTY |  | The spec permitted: RV_stat { 
      | st_dev | = | 2049; |  | st_ino | = | 2; |  | st_kind | = | S_IFDIR; |  | st_perm | = | 0o755; |  | st_nlink | = | 2; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 9999; |  }
 |  | expected st_nlink 2 but got st_nlink 1 |  | 
  
    
    | 71 | 
 | 
  
    
    | 72 | stat "/nonempty_dir2" | 
  
    
    | 73 | Tau | 
  
    
    
    | 74 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 295290; |  | st_kind | = | S_IFDIR; |  | st_perm | = | 0o755; |  | st_nlink | = | 1; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 1; |  } | 
  
    |  | 
      | THE SPEC ASSERTS THE STATE SET IS EMPTY |  | The spec permitted: RV_stat { 
      | st_dev | = | 2049; |  | st_ino | = | 3; |  | st_kind | = | S_IFDIR; |  | st_perm | = | 0o755; |  | st_nlink | = | 3; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 9999; |  }
 |  | expected st_nlink 3 but got st_nlink 1 |  | 
  
    
    | 75 | 
 | 
  
    
    | 76 | stat "/nonempty_dir2/mydir" | 
  
    
    | 77 | Tau | 
  
    
    
    | 78 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 295293; |  | st_kind | = | S_IFDIR; |  | st_perm | = | 0o755; |  | st_nlink | = | 1; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 0; |  } | 
  
    |  | 
      | THE SPEC ASSERTS THE STATE SET IS EMPTY |  | The spec permitted: RV_stat { 
      | st_dev | = | 2049; |  | st_ino | = | 4; |  | st_kind | = | S_IFDIR; |  | st_perm | = | 0o755; |  | st_nlink | = | 2; |  | st_uid | = | 0; |  | st_gid | = | 0; |  | st_rdev | = | 0; |  | st_size | = | 9999; |  }
 |  | expected st_nlink 2 but got st_nlink 1 |  | 
  
    
    | 79 | 
 | 
  
    
    | 80 | 
 |