--- a/Flask.thy	Wed May 08 10:00:38 2013 +0800
+++ b/Flask.thy	Thu May 09 11:19:44 2013 +0800
@@ -158,6 +158,7 @@
 
   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"
   and init_msgs_distinct:      "\<And> q. distinct (init_msgs_of_queue q)"
+  and init_msgs_valid:         "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs"
 
   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"
   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)"
@@ -735,11 +736,15 @@
                                   (\<exists> fd. obj = O_udp_sock (p', fd) \<and> is_udp_sock s (p',fd)) \<or>
                                   deleted obj s)"
 | "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>
-                                     (obj = O_udp_sock (p,fd) \<and> is_udp_sock s (p, fd)) \<or> deleted obj s)"
+                                     (obj = O_udp_sock (p,fd) \<and> is_udp_sock s (p, fd)) \<or> 
+                                     (\<exists> f. obj = O_file f \<and> proc_fd_of_file s f = {(p, fd)} \<and> 
+                                           f \<in> files_hung_by_del s) \<or> deleted obj s)"
 | "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> 
                                        (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd) \<and> fd \<notin> fds) \<or>
                                        (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd) \<and> fd \<notin> fds) \<or>
                                        deleted obj s)"
+| "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> 
+                                            deleted obj s)"
 | "deleted obj (UnLink p f # s) = ((obj = O_file f) \<or> deleted obj s)"
 | "deleted obj (Rmdir p f # s)  = ((obj = O_dir  f) \<or> deleted obj s)"
 | "deleted obj (Exit p # s) = ((obj = O_proc p) \<or> (\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd) \<or>