| 1 | 
  
    
    | 2 | @type trace | 
  
    
    | 3 | 
 | 
  
    
    | 4 | 
  
    
    | 5 | 
  
    
    | 6 | 
  
    
    | 7 | 
 | 
  
    
    | 8 | 
  
    
    | 9 | 
 | 
  
    
    | 10 | mkdir "/dir1" 0o777 | 
  
    
    | 11 | Tau | 
  
    
    | 12 | RV_none | 
  
    
    | 13 | stat "/dir1" | 
  
    
    | 14 | Tau | 
  
    
    
    | 15 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 286799; |  | 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 | = | 1; |  | 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 |  | 
  
    
    | 16 | mkdir "/dir1/subdir1" 0o777 | 
  
    
    | 17 | Tau | 
  
    
    | 18 | RV_none | 
  
    
    | 19 | stat "/dir1" | 
  
    
    | 20 | Tau | 
  
    
    
    | 21 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 286799; |  | 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 | = | 1; |  | 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 |  | 
  
    
    | 22 | stat "/dir1/subdir1" | 
  
    
    | 23 | Tau | 
  
    
    
    | 24 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 286801; |  | 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 |  | 
  
    
    | 25 | 
 | 
  
    
    | 26 | rmdir "/dir1/subdir1" | 
  
    
    | 27 | Tau | 
  
    
    | 28 | RV_none | 
  
    
    | 29 | stat "/dir1" | 
  
    
    | 30 | Tau | 
  
    
    
    | 31 | RV_stat { 
      | st_dev | = | 42; |  | st_ino | = | 286799; |  | 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 | = | 1; |  | 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 |  | 
  
    
    | 32 | 
 | 
  
    
    | 33 | 
 | 
  
    
    | 34 | 
 |