--- a/no_shm_selinux/Static.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Static.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -77,6 +77,7 @@
 where
   "init_o2s_afs f \<equiv> {sec. \<exists> f'. f' \<preceq> f \<and> init_sectxt_of_obj (O_dir f') = Some sec}" *)
 
+(*
 definition init_cm2smsg :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
 where
   "init_cm2smsg q m \<equiv> (case (init_sectxt_of_obj (O_msg q m)) of 
@@ -96,6 +97,7 @@
   "init_cq2smsgq q \<equiv> (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of 
        (Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms)
      | _ \<Rightarrow> None)"
+*)
 
 fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option"
 where
@@ -110,11 +112,13 @@
      (case (init_cf2sfile f) of
            Some sf \<Rightarrow> Some (S_dir sf) 
          | _ \<Rightarrow> None)"
-| "init_obj2sobj (O_msgq q) = 
+| "init_obj2sobj (O_msgq q) = None"
+
+(*
      (case (init_cq2smsgq q) of
        Some sq \<Rightarrow> Some (S_msgq sq)
      | _ \<Rightarrow> None)"
-(*
+
 | "init_obj2sobj (O_shm h) = 
      (case (init_ch2sshm h) of 
        Some sh \<Rightarrow> Some (S_shm sh)
@@ -184,6 +188,7 @@
        cpfd2sfds s p)
                    | _ \<Rightarrow> None)"
 
+(*
 definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
 where
   "cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of 
@@ -191,6 +196,13 @@
  Some (if (\<not> died (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q)) then Init m else Created,
        sec, O_msg q m \<in> tainted s)
                     | _ \<Rightarrow> None)"
+*)
+
+definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
+where
+  "cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of 
+                      Some sec \<Rightarrow> Some (Created, sec, O_msg q m \<in> tainted s)
+                    | _ \<Rightarrow> None)"
 
 fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
 where 
@@ -199,7 +211,7 @@
      (case (cqm2sms s q ms, cm2smsg s q m) of 
        (Some sms, Some sm) \<Rightarrow> Some (sm#sms) 
      | _ \<Rightarrow> None)"
-
+(*
 definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
 where
   "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of 
@@ -207,6 +219,13 @@
  Some (if (\<not> died (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created,
        sec, sms)
                    | _ \<Rightarrow> None)"
+*)
+
+definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
+where
+  "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of 
+                     (Some sec, Some sms) \<Rightarrow> Some (Created, sec, sms)
+                   | _ \<Rightarrow> None)"
 
 fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option"
 where
@@ -266,22 +285,24 @@
   "is_many_sproc (Created, sec,fds) = True"
 | "is_many_sproc _                       = False"
 
+(*
 fun is_many_smsg :: "t_smsg \<Rightarrow> bool"
 where
   "is_many_smsg (Created,sec,tag) = True"
 | "is_many_smsg _                 = False"
-
+*)
 (* wrong def 
 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
 where
   "is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))"
 | "is_many_smsgq _                 = False"
 *)
-
+(*
 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
 where
   "is_many_smsgq (Created,sec,sms) = True"
 | "is_many_smsgq _                 = False"
+*)
 (*
 fun is_many_sshm :: "t_sshm \<Rightarrow> bool"
 where
@@ -293,16 +314,17 @@
   "is_many (S_proc sp   tag) = is_many_sproc sp"
 | "is_many (S_file sfs  tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
 | "is_many (S_dir  sf      ) = is_many_sfile sf"
-| "is_many (S_msgq sq      ) = is_many_smsgq sq"
+| "is_many (S_msgq sq      ) = True"
 (*
 | "is_many (S_shm  sh      ) = is_many_sshm  sh"
 *)
 
+(*
 fun is_init_smsgq :: "t_smsgq \<Rightarrow> bool"
 where
   "is_init_smsgq (Init q,sec,sms) = True"
 | "is_init_smsgq _                = False"
-
+*)
 (*
 fun is_init_sshm :: "t_sshm \<Rightarrow> bool"
 where
@@ -314,7 +336,7 @@
   "is_init_sobj (S_proc sp tag ) = is_init_sproc sp"
 | "is_init_sobj (S_file sfs tag) = (\<exists> sf \<in> sfs. is_init_sfile sf)"
 | "is_init_sobj (S_dir  sf     ) = is_init_sfile sf"
-| "is_init_sobj (S_msgq sq     ) = is_init_smsgq sq"
+| "is_init_sobj (S_msgq sq     ) = False"
 (*
 | "is_init_sobj (S_shm  sh     ) = is_init_sshm sh"
 *)