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 sfd 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 f. init_file_of_proc_fd p fd = Some f \<and> 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) |
56 | _ \<Rightarrow> None)" |
56 | _ \<Rightarrow> None)" |
57 |
57 |
58 definition init_cph2spshs |
58 definition init_cph2spshs |
59 :: "t_process \<Rightarrow> (t_sshm \<times> t_shm_attach_flag) set" |
59 :: "t_process \<Rightarrow> (t_sshm \<times> t_shm_attach_flag) set" |
60 where |
60 where |
61 "init_cph2spshs p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> init_procs_of_shm h \<and> |
61 "init_cph2spshs p \<equiv> {(sh, flag). \<exists> h. (p, flag) \<in> init_procs_of_shm h \<and> |
62 init_ch2sshm h = Some sh}" |
62 init_ch2sshm h = Some sh}" |
63 |
63 |
64 definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option" |
64 definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option" |
65 where |
65 where |
66 "init_cp2sproc p \<equiv> (case (init_sectxt_of_obj (O_proc p)) of |
66 "init_cp2sproc p \<equiv> (case (init_sectxt_of_obj (O_proc p)) of |