--- a/S2ss_prop.thy	Wed Aug 28 08:59:12 2013 +0800
+++ b/S2ss_prop.thy	Thu Aug 29 10:01:24 2013 +0800
@@ -4,4 +4,9 @@
 begin
 (*>*)
 
-context tainting_s begin
\ No newline at end of file
+context tainting_s begin
+
+(* simpset for s2ss*)
+
+lemma s2ss_execve:
+  "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = s2ss s "
\ No newline at end of file

--- a/Static.thy	Wed Aug 28 08:59:12 2013 +0800
+++ b/Static.thy	Thu Aug 29 10:01:24 2013 +0800
@@ -592,7 +592,9 @@
                S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss;
                permission_check pctxt qctxt C_msgq P_read; 
                permission_check pctxt mctxt C_msg  P_receive\<rbrakk>
-  \<Longrightarrow> (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm)) \<in> static"
+  \<Longrightarrow> (update_ss (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm)) 
+                 (S_msgq (qi, qctxt, (mi, mctxt, tagm)#sms))
+                 (S_msgq (qi, qctxt, sms))) \<in> static"
 | s_removeq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;
                permission_check pctxt qctxt C_msgq P_destroy\<rbrakk>
   \<Longrightarrow> (del_ss ss (S_msgq (qi,qctxt,sms))) \<in> static"
@@ -786,10 +788,12 @@
      (case (ch2sshm s h) of 
         Some sh \<Rightarrow> Some (S_shm sh)
       | _ \<Rightarrow> None)"
+(*
 | "co2sobj s (O_msg q m) = 
      (case (cq2smsgq s q, cm2smsg s q m) of 
        (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
      | _ \<Rightarrow> None)"
+*)
 | "co2sobj s _ = None"