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/Flask.thy
changeset 83 e79e3a8a4ceb
parent 82 0a68c605ae79
child 87 8d18cfc845dd 
--- a/no_shm_selinux/Flask.thy	Mon Dec 23 19:47:17 2013 +0800
+++ b/no_shm_selinux/Flask.thy	Thu Dec 26 10:56:50 2013 +0800
@@ -510,7 +510,7 @@
   "info_flow_shm s from to \<equiv> (self_shm s from to) \<or> (\<exists> h. one_flow_shm s h from to)" 
 *)
 
-fun current_msgqs :: "t_state \<Rightarrow> t_msg set"
+fun current_msgqs :: "t_state \<Rightarrow> t_msgq set"
 where
   "current_msgqs [] = init_msgqs"
 | "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)"
selinux