diff -r 01274a64aece -r aa1375b6c0eb Flask.thy
--- a/Flask.thy	Mon Aug 05 12:30:26 2013 +0800
+++ b/Flask.thy	Tue Aug 27 08:50:53 2013 +0800
@@ -705,7 +705,7 @@
 | "os_grant \<tau> (SendMsg p q m)                 = 
     (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m \<notin> (set (msgs_of_queue \<tau> q)))"
 | "os_grant \<tau> (RecvMsg p q m)                 = 
-    (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m = hd (msgs_of_queue \<tau> q))"
+    (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m = hd (msgs_of_queue \<tau> q) \<and> msgs_of_queue \<tau> q \<noteq> [])"
 | "os_grant \<tau> (RemoveMsgq p q)                = 
     (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau>)"
 | "os_grant \<tau> (CreateShM p h)                 = 
@@ -1475,7 +1475,7 @@
 | t_attach1:"\<lbrakk>O_proc p \<in> tainted s; valid (Attach p h SHM_RDWR # s); (p', flag') \<in> procs_of_shm s h\<rbrakk>
              \<Longrightarrow> O_proc p' \<in> tainted (Attach p h SHM_RDWR # s)"
 | t_attach2:"\<lbrakk>O_proc p' \<in> tainted s; valid (Attach p h flag # s); (p', SHM_RDWR) \<in> procs_of_shm s h\<rbrakk>
-             \<Longrightarrow> O_proc p \<in> tainted (Attach p h SHM_RDWR # s)"
+             \<Longrightarrow> O_proc p \<in> tainted (Attach p h flag # s)"
 | t_sendmsg:"\<lbrakk>O_proc p \<in> tainted s; valid (SendMsg p q m # s)\<rbrakk>
              \<Longrightarrow> O_msg q m \<in> tainted (SendMsg p q m # s)"
 | t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'\<rbrakk>