--- a/Co2sobj_prop.thy	Wed Sep 04 09:58:30 2013 +0800
+++ b/Co2sobj_prop.thy	Wed Sep 04 15:13:54 2013 +0800
@@ -1831,6 +1831,23 @@
 (* simpset for co2sobj *)
 
 lemma co2sobj_execve:
+  "\<lbrakk>valid (Execve p f fds # s); alive (Execve p f fds # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
+      if (obj = O_proc p)
+      then (case (cp2sproc (Execve p f fds # s) p) of
+              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s))
+            | _       \<Rightarrow> None) 
+      else co2sobj s obj )"
+apply (frule vt_grant_os, frule vd_cons, case_tac obj)
+apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (case_tac "cp2sproc (Execve p f fds # s) p")
+apply (drule current_proc_has_sp', simp, simp)
+apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits)
+apply (simp add:is_dir_simps, frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_dir_in_current)
+done
+
+lemma co2sobj_execve':
   "\<lbrakk>valid (Execve p f fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
       if (obj = O_proc p)
       then (case (cp2sproc (Execve p f fds # s) p) of
@@ -1847,7 +1864,7 @@
 apply (simp add:is_dir_in_current)
 done
 
-lemma co2sobj_clone:
+lemma co2sobj_clone':
   "\<lbrakk>valid (Clone p p' fds shms # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds shms # s) obj = (
       if (obj = O_proc p')
       then (case (cp2sproc (Clone p p' fds shms # s) p') of
@@ -1867,6 +1884,32 @@
 apply (simp add:is_dir_in_current)
 done
 
+lemma co2sobj_clone:
+  "\<lbrakk>valid (Clone p p' fds shms # s); alive (Clone p p' fds shms # s) obj\<rbrakk> 
+   \<Longrightarrow> co2sobj (Clone p p' fds shms # s) obj = (
+      if (obj = O_proc p')
+      then (case (cp2sproc (Clone p p' fds shms # s) p') of
+              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+            | _       \<Rightarrow> None)
+      else co2sobj s obj )"
+apply (frule vt_grant_os, frule vd_cons, case_tac obj)
+apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other 
+  cq2smsgq_other tainted_eq_Tainted)
+apply (rule conjI, rule impI, simp)
+apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'")
+apply (drule current_proc_has_sp', simp, simp)
+apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp)
+apply (simp add:tainted_eq_Tainted, rule impI, rule notI)
+apply (drule Tainted_in_current, simp+)
+apply (rule impI, simp)
+apply (drule current_proc_has_sp, simp, (erule exE|erule conjE)+)
+apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted Tainted_in_current split:option.splits)
+
+apply (simp add:is_dir_simps, frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_dir_in_current)
+done
+
 lemma co2sobj_ptrace:
   "\<lbrakk>valid (Ptrace p p' # s); alive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (
      case obj of
@@ -2201,7 +2244,13 @@
 done
 
 lemma co2sobj_createshm:
-  "\<lbrakk>valid (CreateShM p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = co2sobj s obj"
+  "\<lbrakk>valid (CreateShM p h # s); alive (CreateShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = (
+      case obj of 
+        O_shm h' \<Rightarrow> if (h' = h) then (case (ch2sshm (CreateShM p h # s) h) of
+                                        Some sh \<Rightarrow> Some (S_shm sh)
+                                      | _       \<Rightarrow> None)
+                    else co2sobj s obj
+      | _        \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
@@ -2318,6 +2367,8 @@
   co2sobj_truncate co2sobj_kill co2sobj_exit co2sobj_createmsgq co2sobj_sendmsg co2sobj_recvmsg
   co2sobj_removemsgq co2sobj_attach co2sobj_detach co2sobj_createshm co2sobj_deleteshm
 
+
+
 end
 
 (*<*)