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 20 e2c6af3ccb0d
parent 19 ced0fcfbcf8e
child 25 259a50be4381
equal deleted inserted replaced
19:ced0fcfbcf8e 20:e2c6af3ccb0d 
   651 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool"
 
   651 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool"
 
   652 where
 
   652 where
 
   653   "tainted_s ss (S_proc sp  tag) = (S_proc sp tag  \<in> ss \<and> tag = True)"
 
   653   "tainted_s ss (S_proc sp  tag) = (S_proc sp tag  \<in> ss \<and> tag = True)"
 
   654 | "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)"
 
   654 | "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)"
 
   655 | "tainted_s ss (S_msg  (qi, sec, sms)  (mi, secm, tag)) = 
   655 | "tainted_s ss (S_msg  (qi, sec, sms)  (mi, secm, tag)) = 
   656      (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,sec,tag) \<in> set sms \<and> tag = True)"
 
   656      (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,secm,tag) \<in> set sms \<and> tag = True)"
 
   657 | "tainted_s ss _ = False"
 
   657 | "tainted_s ss _ = False"
 
   658 
   658 
   659 (*
 
   659 (*
 
   660 fun tainted_s :: "t_object \<Rightarrow> t_static_state \<Rightarrow> bool"
 
   660 fun tainted_s :: "t_object \<Rightarrow> t_static_state \<Rightarrow> bool"
 
   661 where 
   661 where
selinux