--- a/no_shm_selinux/Flask.thy	Wed Dec 18 10:44:36 2013 +0800
+++ b/no_shm_selinux/Flask.thy	Thu Dec 19 10:05:13 2013 +0800
@@ -550,9 +550,13 @@
 | "flags_of_proc_fd (Accept p fd addr lport' fd' ino # \<tau>) p' fd'' = 
      (if (p = p' \<and> fd' = fd'') then None else flags_of_proc_fd \<tau> p' fd'')"
 | "flags_of_proc_fd (Clone p p' fds # \<tau>) p'' fd = 
-     (if (p' = p'' \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p'' fd)"  
+     (if (p' = p'' \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd 
+      else if (p' = p'') then None
+      else flags_of_proc_fd \<tau> p'' fd)"  
 | "flags_of_proc_fd (Execve p f fds # \<tau>) p' fd = 
-     (if (p' = p \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p' fd)"
+     (if (p' = p \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd 
+      else if (p' = p) then None
+      else flags_of_proc_fd \<tau> p' fd)"
 | "flags_of_proc_fd (Kill p\<^isub>1 p\<^isub>2 # \<tau>) p fd = 
      (if (p = p\<^isub>2) then None else flags_of_proc_fd \<tau> p fd)"
 | "flags_of_proc_fd (Exit p # \<tau>) p' fd' =