| 1 | 
  
    
    | 2 | @type trace | 
  
    
    | 3 | 
  
    
    | 4 | 
  
    
    | 5 | 
  
    
    | 6 | 
 | 
  
    
    | 7 | Pid 2 -> create (User_id 1) (Group_id 1) | 
  
    
    | 8 | add_user_to_group (User_id 1) (Group_id 1) | 
  
    
    | 9 | Tau | 
  
    
    | 10 | RV_none | 
  
    
    | 11 | Pid 2 -> umask 0o000 | 
  
    
    | 12 | Tau | 
  
    
    | 13 | RV_file_perm(0o022) | 
  
    
    | 14 | 
 | 
  
    
    | 15 | Pid 3 -> create (User_id 2) (Group_id 2) | 
  
    
    | 16 | add_user_to_group (User_id 2) (Group_id 2) | 
  
    
    | 17 | Tau | 
  
    
    | 18 | RV_none | 
  
    
    | 19 | Pid 3 -> umask 0o000 | 
  
    
    | 20 | Tau | 
  
    
    | 21 | RV_file_perm(0o022) | 
  
    
    | 22 | 
 | 
  
    
    | 23 | Pid 2 -> mkdir "/d" 0o755 | 
  
    
    | 24 | Tau | 
  
    
    | 25 | RV_none | 
  
    
    | 26 | Pid 2 -> open_close "/d/f" [O_CREAT;O_RDWR] 0o004 | 
  
    
    | 27 | Tau | 
  
    
    | 28 | RV_none | 
  
    
    | 29 | Pid 2 -> chown "/d/f" (User_id 1) (Group_id 1) | 
  
    
    | 30 | Tau | 
  
    
    | 31 | RV_none | 
  
    
    | 32 | 
 | 
  
    
    | 33 | Pid 3 -> open_close "/d/f" [O_RDONLY] | 
  
    
    | 34 | Tau | 
  
    
    | 35 | RV_none | 
  
    
    | 36 | Pid 3 -> open_close "/d/f" [O_WRONLY] | 
  
    
    | 37 | Tau | 
  
    
    | 38 | EACCES | 
  
    
    | 39 | Pid 3 -> open_close "/d/f" [O_RDWR] | 
  
    
    | 40 | Tau | 
  
    
    | 41 | EACCES | 
  
    
    | 42 | Pid 3 -> open_close "/d/f" [O_RDONLY;O_TRUNC] | 
  
    
    | 43 | Tau | 
  
    
    | 44 | EACCES | 
  
    
    | 45 | Pid 3 -> open_close "/d/f" [O_TRUNC;O_WRONLY] | 
  
    
    | 46 | Tau | 
  
    
    | 47 | EACCES | 
  
    
    | 48 | Pid 3 -> open_close "/d/f" [O_RDONLY;O_APPEND] | 
  
    
    | 49 | Tau | 
  
    
    | 50 | RV_none | 
  
    
    | 51 | Pid 3 -> open_close "/d/f" [O_APPEND;O_WRONLY] | 
  
    
    | 52 | Tau | 
  
    
    | 53 | EACCES | 
  
    
    | 54 | 
 | 
  
    
    | 55 | dump-result / 
    
      | / | D | 32642 |  |  |  
      | /d | D | 32645 |  |  |  
      | /d/f | F | 12 | 0 | da39a3ee5e6b4b0d3255bfef95601890afd80709 |  | 
  
    
    | 56 | 
 | 
  
    
    | 57 | 
 |