97 "init_obj2sobj (O_proc p) = |
97 "init_obj2sobj (O_proc p) = |
98 (case (init_cp2sproc p) of |
98 (case (init_cp2sproc p) of |
99 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds)) |
99 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds)) |
100 | _ \<Rightarrow> None)" |
100 | _ \<Rightarrow> None)" |
101 | "init_obj2sobj (O_file f) = |
101 | "init_obj2sobj (O_file f) = |
102 (if (f \<in> init_files \<and> is_init_file f) |
102 Some (S_file (init_cf2sfiles f) |
103 then Some (S_file (init_cf2sfiles f) |
103 (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))" |
104 (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds)) |
104 | "init_obj2sobj (O_dir f) = |
105 else None)" |
105 (case (init_cf2sfile f) of |
106 | "init_obj2sobj (O_dir f) = |
106 Some sf \<Rightarrow> Some (S_dir sf) |
107 (if (is_init_dir f) then |
107 | _ \<Rightarrow> None)" |
108 (case (init_cf2sfile f) of |
|
109 Some sf \<Rightarrow> Some (S_dir sf) |
|
110 | _ \<Rightarrow> None) |
|
111 else None)" |
|
112 | "init_obj2sobj (O_msgq q) = |
108 | "init_obj2sobj (O_msgq q) = |
113 (case (init_cq2smsgq q) of |
109 (case (init_cq2smsgq q) of |
114 Some sq \<Rightarrow> Some (S_msgq sq) |
110 Some sq \<Rightarrow> Some (S_msgq sq) |
115 | _ \<Rightarrow> None)" |
111 | _ \<Rightarrow> None)" |
116 | "init_obj2sobj (O_shm h) = |
112 | "init_obj2sobj (O_shm h) = |
771 "co2sobj s (O_proc p) = |
767 "co2sobj s (O_proc p) = |
772 (case (cp2sproc s p) of |
768 (case (cp2sproc s p) of |
773 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s)) |
769 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s)) |
774 | _ \<Rightarrow> None)" |
770 | _ \<Rightarrow> None)" |
775 | "co2sobj s (O_file f) = |
771 | "co2sobj s (O_file f) = |
776 (if (f \<in> current_files s) then |
772 Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))" |
777 Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s)) |
|
778 else None)" |
|
779 | "co2sobj s (O_dir f) = |
773 | "co2sobj s (O_dir f) = |
780 (case (cf2sfile s f) of |
774 (case (cf2sfile s f) of |
781 Some sf \<Rightarrow> Some (S_dir sf) |
775 Some sf \<Rightarrow> Some (S_dir sf) |
782 | _ \<Rightarrow> None)" |
776 | _ \<Rightarrow> None)" |
783 | "co2sobj s (O_msgq q) = |
777 | "co2sobj s (O_msgq q) = |