548 | "flags_of_proc_fd (CreateSock p af st fd ino # \<tau>) p' fd' = |
548 | "flags_of_proc_fd (CreateSock p af st fd ino # \<tau>) p' fd' = |
549 (if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')" |
549 (if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')" |
550 | "flags_of_proc_fd (Accept p fd addr lport' fd' ino # \<tau>) p' fd'' = |
550 | "flags_of_proc_fd (Accept p fd addr lport' fd' ino # \<tau>) p' fd'' = |
551 (if (p = p' \<and> fd' = fd'') then None else flags_of_proc_fd \<tau> p' fd'')" |
551 (if (p = p' \<and> fd' = fd'') then None else flags_of_proc_fd \<tau> p' fd'')" |
552 | "flags_of_proc_fd (Clone p p' fds # \<tau>) p'' fd = |
552 | "flags_of_proc_fd (Clone p p' fds # \<tau>) p'' fd = |
553 (if (p' = p'' \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p'' fd)" |
553 (if (p' = p'' \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd |
|
554 else if (p' = p'') then None |
|
555 else flags_of_proc_fd \<tau> p'' fd)" |
554 | "flags_of_proc_fd (Execve p f fds # \<tau>) p' fd = |
556 | "flags_of_proc_fd (Execve p f fds # \<tau>) p' fd = |
555 (if (p' = p \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p' fd)" |
557 (if (p' = p \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd |
|
558 else if (p' = p) then None |
|
559 else flags_of_proc_fd \<tau> p' fd)" |
556 | "flags_of_proc_fd (Kill p\<^isub>1 p\<^isub>2 # \<tau>) p fd = |
560 | "flags_of_proc_fd (Kill p\<^isub>1 p\<^isub>2 # \<tau>) p fd = |
557 (if (p = p\<^isub>2) then None else flags_of_proc_fd \<tau> p fd)" |
561 (if (p = p\<^isub>2) then None else flags_of_proc_fd \<tau> p fd)" |
558 | "flags_of_proc_fd (Exit p # \<tau>) p' fd' = |
562 | "flags_of_proc_fd (Exit p # \<tau>) p' fd' = |
559 (if (p = p') then None else flags_of_proc_fd \<tau> p' fd')" |
563 (if (p = p') then None else flags_of_proc_fd \<tau> p' fd')" |
560 | "flags_of_proc_fd (e # \<tau>) p fd = flags_of_proc_fd \<tau> p fd" |
564 | "flags_of_proc_fd (e # \<tau>) p fd = flags_of_proc_fd \<tau> p fd" |