equal
deleted
inserted
replaced
45 | _ \<Rightarrow> None) |
45 | _ \<Rightarrow> None) |
46 | _ \<Rightarrow> None)" |
46 | _ \<Rightarrow> None)" |
47 |
47 |
48 definition init_cfds2sfds :: "t_process \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) set" |
48 definition init_cfds2sfds :: "t_process \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) set" |
49 where |
49 where |
50 "init_cfds2sfds p \<equiv> { sfd. \<exists> fd f. init_file_of_proc_fd p fd = Some f \<and> init_cfd2sfd p fd = Some sfd}" |
50 "init_cfds2sfds p \<equiv> { sfd. \<exists> fd \<in> init_proc_file_fds p. init_cfd2sfd p fd = Some sfd}" |
51 |
51 |
52 definition init_ch2sshm :: "t_shm \<Rightarrow> t_sshm option" |
52 definition init_ch2sshm :: "t_shm \<Rightarrow> t_sshm option" |
53 where |
53 where |
54 "init_ch2sshm h \<equiv> (case (init_sectxt_of_obj (O_shm h)) of |
54 "init_ch2sshm h \<equiv> (case (init_sectxt_of_obj (O_shm h)) of |
55 Some sec \<Rightarrow> Some (Init h, sec) |
55 Some sec \<Rightarrow> Some (Init h, sec) |
710 | _ \<Rightarrow> None)" |
710 | _ \<Rightarrow> None)" |
711 |
711 |
712 |
712 |
713 definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set" |
713 definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set" |
714 where |
714 where |
715 "cpfd2sfds s p \<equiv> {sfd. \<exists> fd f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}" |
715 "cpfd2sfds s p \<equiv> {sfd. \<exists> fd \<in> proc_file_fds s p. cfd2sfd s p fd = Some sfd}" |
716 |
716 |
717 definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option" |
717 definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option" |
718 where |
718 where |
719 "ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of |
719 "ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of |
720 Some sec \<Rightarrow> |
720 Some sec \<Rightarrow> |