--- a/no_shm_selinux/Flask.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Flask.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -135,8 +135,11 @@
 *)
   and init_socket_state ::      "t_socket \<rightharpoonup> t_sock_state"
 
+(*
   and init_msgqs :: "t_msgq set"
   and init_msgs_of_queue:: "t_msgq \<Rightarrow> t_msg list"
+*)
+  and max_queue :: "nat"
 (*
   and init_shms :: "t_shm set"
   and init_procs_of_shm :: "t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set" 
@@ -162,8 +165,12 @@
   and init_procs_has_shm:      "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms \<and> init_flag_of_proc_shm p h = Some flag"
   and init_shmflag_has_proc:   "\<And> p h flag. init_flag_of_proc_shm p h = Some flag \<Longrightarrow> (p, flag) \<in> init_procs_of_shm h"
 *)
+
+(*
   and init_msgs_distinct:      "\<And> q. distinct (init_msgs_of_queue q)"
   and init_msgs_valid:         "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs"
+  and init_msgq_valid:         "\<And> q. length (init_msgs_of_queue q) \<le> max_queue"
+*)
 
   and init_socket_has_inode:   "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p \<and> init_file_of_proc_fd p fd = None"
   and inos_has_sock_tag:  "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)"
@@ -174,7 +181,7 @@
   and init_netobj_has_raddr:   "\<And> s. after_conacc (init_netobj_state s) \<Longrightarrow> init_netobj_remoteaddr s \<noteq> None"
 *)
 
-  and init_finite_sets:   "finite init_files \<and> finite init_procs \<and> (\<forall> p. finite (init_fds_of_proc p)) \<and> finite init_shms \<and> finite init_msgqs \<and> finite init_users" 
+  and init_finite_sets:   "finite init_files \<and> finite init_procs \<and> (\<forall> p. finite (init_fds_of_proc p)) \<and> finite init_shms \<and> finite init_users"  (* finite init_msgqs *)
 
 begin 
 
@@ -226,8 +233,8 @@
 (*
 | "init_alive (O_shm  h)     = (h \<in> init_shms)"
 *)
-| "init_alive (O_msgq q)     = (q \<in> init_msgqs)"
-| "init_alive (O_msg q m)    = (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)"
+| "init_alive (O_msgq q)     = False" (* (q \<in> init_msgqs) *)
+| "init_alive (O_msg q m)    = False" (* (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)" *)
 
 
 (************ system listeners, event-related ***********)
@@ -512,14 +519,14 @@
 
 fun current_msgqs :: "t_state \<Rightarrow> t_msgq set"
 where
-  "current_msgqs [] = init_msgqs"
+  "current_msgqs [] = {}" (* init_msgqs *)
 | "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)"
 | "current_msgqs (RemoveMsgq p q # \<tau>) = (current_msgqs \<tau>) - {q}"
 | "current_msgqs (_ # \<tau>) = current_msgqs \<tau>"
 
 fun msgs_of_queue :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list"
 where
-  "msgs_of_queue [] = init_msgs_of_queue"
+  "msgs_of_queue [] = (\<lambda> x. [])" (* init_msgs_of_queue*)
 | "msgs_of_queue (CreateMsgq p q # \<tau>) = (msgs_of_queue \<tau>)(q := [])"
 | "msgs_of_queue (SendMsg p q m  # \<tau>) = (msgs_of_queue \<tau>)(q := msgs_of_queue \<tau> q @ [m])"
 | "msgs_of_queue (RecvMsg p q m  # \<tau>) = (msgs_of_queue \<tau>)(q := tl (msgs_of_queue \<tau> q))"
@@ -720,7 +727,8 @@
 | "os_grant \<tau> (CreateMsgq p q)                = 
     (p \<in> current_procs \<tau> \<and> q \<notin> (current_msgqs \<tau>))"
 | "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)))"
+    (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m \<notin> (set (msgs_of_queue \<tau> q)) \<and> 
+     length (msgs_of_queue \<tau> q) < max_queue)"
 | "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) \<and> msgs_of_queue \<tau> q \<noteq> [])"
 | "os_grant \<tau> (RemoveMsgq p q)                = 
@@ -1477,7 +1485,8 @@
   "valid []"
 | "\<lbrakk>valid s; os_grant s e; grant s e\<rbrakk> \<Longrightarrow> valid (e # s)"
 
-(* tobj: object that can be tainted *)
+
+(* tobj: object that can be tainted 
 fun tobj_in_init :: "t_object \<Rightarrow> bool"
 where
   "tobj_in_init (O_proc p) = (p \<in> init_procs)"
@@ -1489,6 +1498,8 @@
 | "tobj_in_init (O_msg q m) = (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)"
 *)
 | "tobj_in_init _ = False" (* other kind of obj cannot be tainted *)
+*)
+
 
 (* no use
 fun no_del_event:: "t_event list \<Rightarrow> bool"