no_shm_selinux/Flask.thy
changeset 78 030643fab8a1
parent 77 6f7b9039715f
child 79 c09fcbcdb871
--- a/no_shm_selinux/Flask.thy	Tue Dec 17 13:30:21 2013 +0800
+++ b/no_shm_selinux/Flask.thy	Wed Dec 18 10:44:36 2013 +0800
@@ -1378,7 +1378,7 @@
        Some pf \<Rightarrow> 
          (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of 
            (Some (pu,pr,pt), Some (du,dr,dt)) \<Rightarrow> 
-             (search_check s (pu,pr,pt) f \<and> 
+             (search_check s (pu,pr,pt) pf \<and> 
               permission_check (pu,pr,pt) (nfctxt_create (pu,pr,pt) (du,dr,dt) C_dir) C_dir P_create \<and>
               permission_check (pu,pr,pt) (du,dr,dt) C_dir P_add_name)
          | _ \<Rightarrow> False)