156 and init_filefd_valid: "\<And> p fd f. init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p \<and> (\<exists> im. init_inum_of_file f = Some im \<and> init_itag_of_inum im = Some Tag_FILE) \<and> p \<in> init_procs \<and> (\<exists> flags. init_oflags_of_proc_fd p fd = Some flags)" |
156 and init_filefd_valid: "\<And> p fd f. init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p \<and> (\<exists> im. init_inum_of_file f = Some im \<and> init_itag_of_inum im = Some Tag_FILE) \<and> p \<in> init_procs \<and> (\<exists> flags. init_oflags_of_proc_fd p fd = Some flags)" |
157 and init_fileflag_valid: "\<And> p fd flags. init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> \<exists> f. init_file_of_proc_fd p fd = Some f" |
157 and init_fileflag_valid: "\<And> p fd flags. init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> \<exists> f. init_file_of_proc_fd p fd = Some f" |
158 |
158 |
159 and init_procs_has_shm: "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms" |
159 and init_procs_has_shm: "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms" |
160 and init_msgs_distinct: "\<And> q. distinct (init_msgs_of_queue q)" |
160 and init_msgs_distinct: "\<And> q. distinct (init_msgs_of_queue q)" |
|
161 and init_msgs_valid: "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs" |
161 |
162 |
162 and init_socket_has_inode: "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p" |
163 and init_socket_has_inode: "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p" |
163 and inos_has_sock_tag: "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)" |
164 and inos_has_sock_tag: "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)" |
164 (* |
165 (* |
165 and init_netobj_has_state: "bidirect_in_init init_netobjs init_netobj_state" |
166 and init_netobj_has_state: "bidirect_in_init init_netobjs init_netobj_state" |
733 | "deleted obj (Kill p p' # s) = ((obj = O_proc p') \<or> (\<exists> fd \<in> current_proc_fds s p'. obj = O_fd p' fd) \<or> |
734 | "deleted obj (Kill p p' # s) = ((obj = O_proc p') \<or> (\<exists> fd \<in> current_proc_fds s p'. obj = O_fd p' fd) \<or> |
734 (\<exists> fd. obj = O_tcp_sock (p', fd) \<and> is_tcp_sock s (p',fd)) \<or> |
735 (\<exists> fd. obj = O_tcp_sock (p', fd) \<and> is_tcp_sock s (p',fd)) \<or> |
735 (\<exists> fd. obj = O_udp_sock (p', fd) \<and> is_udp_sock s (p',fd)) \<or> |
736 (\<exists> fd. obj = O_udp_sock (p', fd) \<and> is_udp_sock s (p',fd)) \<or> |
736 deleted obj s)" |
737 deleted obj s)" |
737 | "deleted obj (CloseFd p fd # s) = ((obj = O_fd p fd) \<or> (obj = O_tcp_sock (p,fd) \<and> is_tcp_sock s (p,fd)) \<or> |
738 | "deleted obj (CloseFd p fd # s) = ((obj = O_fd p fd) \<or> (obj = O_tcp_sock (p,fd) \<and> is_tcp_sock s (p,fd)) \<or> |
738 (obj = O_udp_sock (p,fd) \<and> is_udp_sock s (p, fd)) \<or> deleted obj s)" |
739 (obj = O_udp_sock (p,fd) \<and> is_udp_sock s (p, fd)) \<or> |
|
740 (\<exists> f. obj = O_file f \<and> proc_fd_of_file s f = {(p, fd)} \<and> |
|
741 f \<in> files_hung_by_del s) \<or> deleted obj s)" |
739 | "deleted obj (Execve p f fds # s) = ((\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd \<and> fd \<notin> fds) \<or> |
742 | "deleted obj (Execve p f fds # s) = ((\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd \<and> fd \<notin> fds) \<or> |
740 (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd) \<and> fd \<notin> fds) \<or> |
743 (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd) \<and> fd \<notin> fds) \<or> |
741 (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd) \<and> fd \<notin> fds) \<or> |
744 (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd) \<and> fd \<notin> fds) \<or> |
742 deleted obj s)" |
745 deleted obj s)" |
|
746 | "deleted obj (Clone p p' fds shms # s) = ((\<exists> fd \<in> current_proc_fds s p. obj = O_fd p' fd \<and> fd \<notin> fds) \<or> |
|
747 deleted obj s)" |
743 | "deleted obj (UnLink p f # s) = ((obj = O_file f) \<or> deleted obj s)" |
748 | "deleted obj (UnLink p f # s) = ((obj = O_file f) \<or> deleted obj s)" |
744 | "deleted obj (Rmdir p f # s) = ((obj = O_dir f) \<or> deleted obj s)" |
749 | "deleted obj (Rmdir p f # s) = ((obj = O_dir f) \<or> deleted obj s)" |
745 | "deleted obj (Exit p # s) = ((obj = O_proc p) \<or> (\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd) \<or> |
750 | "deleted obj (Exit p # s) = ((obj = O_proc p) \<or> (\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd) \<or> |
746 (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd)) \<or> |
751 (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd)) \<or> |
747 (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd)) \<or> deleted obj s)" |
752 (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd)) \<or> deleted obj s)" |