--- a/no_shm_selinux/Static.thy	Mon Dec 30 12:01:09 2013 +0800
+++ b/no_shm_selinux/Static.thy	Mon Dec 30 14:04:23 2013 +0800
@@ -36,12 +36,16 @@
 where
   "init_cf2sfiles f \<equiv> {sf. \<exists>f' \<in> init_same_inode_files f. init_cf2sfile f' = Some sf}"
 
+fun remove_create_flag :: "t_open_flags \<Rightarrow> t_open_flags"
+where
+  "remove_create_flag (mflag, oflags) = (mflag, oflags - {OF_CREAT})"
+
 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option"
 where
   "init_cfd2sfd p fd = 
      (case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of
         (Some f, Some flags, Some sec) \<Rightarrow> (case (init_cf2sfile f) of 
-                                             Some sf \<Rightarrow> Some (sec, flags, sf)
+                                             Some sf \<Rightarrow> Some (sec, remove_create_flag flags, sf)
                                            | _ \<Rightarrow> None)
       | _ \<Rightarrow> None)"
 
@@ -151,7 +155,7 @@
   "cfd2sfd s p fd \<equiv> 
     (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of
       (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of 
-                                          Some sf \<Rightarrow> Some (sec, flags, sf)
+                                          Some sf \<Rightarrow> Some (sec, remove_create_flag flags, sf)
                                         | _       \<Rightarrow> None)
     | _ \<Rightarrow> None)"
 
@@ -664,10 +668,6 @@
 where
   "brandnew_proc s \<equiv> next_nat (all_procs s)"
 
-fun remove_create_flag :: "t_open_flags \<Rightarrow> t_open_flags"
-where
-  "remove_create_flag (mflag, oflags) = (mflag, oflags - {OF_CREAT})"
-
 definition new_inode_num :: "t_state \<Rightarrow> nat"
 where
   "new_inode_num \<tau> = next_nat (current_inode_nums \<tau>)"