diff -r 690636b7b6f1 -r 8d18cfc845dd no_shm_selinux/Temp.thy
--- a/no_shm_selinux/Temp.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Temp.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -124,7 +124,7 @@
 | s_sendmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;
                permission_check pctxt qctxt C_msgq P_enqueue;
                permission_check pctxt qctxt C_msgq P_write; 
-               permission_check pctxt pctxt C_msg  P_create\<rbrakk>
+               permission_check pctxt pctxt C_msg  P_create; length sms < max_queue\<rbrakk>
   \<Longrightarrow> (update_ss ss (S_msgq (qi,qctxt,sms)) 
                     (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static"
 | s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss;