Mercurial Mercurial > hg > selinux / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
no_shm_selinux/Enrich.thy
changeset 90 003cac7b8bf5
parent 89 ded3f83f6cb9
child 93 dfde07c7cd6b 
--- a/no_shm_selinux/Enrich.thy	Mon Jan 06 23:07:51 2014 +0800
+++ b/no_shm_selinux/Enrich.thy	Tue Jan 07 22:04:06 2014 +0800
@@ -359,7 +359,7 @@
     and cq2sq: "\<forall> q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq s' q = cq2smsgq s q"
     and ffd_remain: "\<forall> p fd f. file_of_proc_fd s p fd = Some f \<longrightarrow> file_of_proc_fd s' p fd = Some f"
     and fflags_remain: "\<forall> p fd flags. flags_of_proc_fd s p fd = Some flags \<longrightarrow> flags_of_proc_fd s' p fd = Some flags"
-    and sms_remain: "\<forall> q. msgs_of_queue s' q = msgs_of_queue s q"
+    and sms_remain: "\<forall> q. q \<in> current_msgqs s \<longrightarrow> msgs_of_queue s' q = msgs_of_queue s q"
    (* and empty_remain: "\<forall> f. dir_is_empty s f \<longrightarrow> dir_is_empty s' f" *)
     and cfd2sfd: "\<forall> p fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd s' p fd = cfd2sfd s p fd"
     and nodel: "no_del_event (e # s)"
selinux