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.
S2ss_prop.thy
changeset 34 e7f850d1e08e
parent 33 6884b3c9284b
child 35 f2e620d799cf 
--- a/S2ss_prop.thy	Thu Aug 29 10:01:24 2013 +0800
+++ b/S2ss_prop.thy	Thu Aug 29 13:29:32 2013 +0800
@@ -9,4 +9,6 @@
 (* simpset for s2ss*)
 
 lemma s2ss_execve:
-  "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = s2ss s "
\ No newline at end of file
+  "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = (
+     if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))
+     then (case (cp2sproc (Execve p f fds # s)  s2ss s \<union> {} "
\ No newline at end of file
selinux