Mercurial Mercurial > hg > selinux / comparison
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.
Static.thy
changeset 34 e7f850d1e08e
parent 33 6884b3c9284b
child 37 029cccce84b4
equal deleted inserted replaced
33:6884b3c9284b 34:e7f850d1e08e 
   114        Some sq \<Rightarrow> Some (S_msgq sq)
 
   114        Some sq \<Rightarrow> Some (S_msgq sq)
 
   115      | _ \<Rightarrow> None)"
 
   115      | _ \<Rightarrow> None)"
 
   116 | "init_obj2sobj (O_shm h) = 
   116 | "init_obj2sobj (O_shm h) = 
   117      (case (init_ch2sshm h) of 
   117      (case (init_ch2sshm h) of 
   118        Some sh \<Rightarrow> Some (S_shm sh)
 
   118        Some sh \<Rightarrow> Some (S_shm sh)
 
   119      | _       \<Rightarrow> None)"
 
   119      | _       \<Rightarrow> None)"  (*
 
   120 | "init_obj2sobj (O_msg q m) = 
   120 | "init_obj2sobj (O_msg q m) = 
   121      (case (init_cq2smsgq q, init_cm2smsg q m) of 
   121      (case (init_cq2smsgq q, init_cm2smsg q m) of 
   122         (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
 
   122         (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
 
   123       | _                  \<Rightarrow> None)"
 
   123       | _                  \<Rightarrow> None)" *)
 
   124 | "init_obj2sobj _ = None"
 
   124 | "init_obj2sobj _ = None"
 
   125 
   125 
   126 definition  
   126 definition  
   127   "init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}"
 
   127   "init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}"
 
   128 
   128
selinux