Mercurial Mercurial > hg > selinux / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
update
authorchunhan
Tue, 21 May 2013 10:19:51 +0800
changeset 11 3e7617baa6a3
parent 10 ac66d8ba86d9
child 12 47a4b2ae0556
update
Co2sobj_prop.thy file | annotate | diff | comparison | revisions
Init_prop.thy file | annotate | diff | comparison | revisions
ROOT file | annotate | diff | comparison | revisions
Static.thy file | annotate | diff | comparison | revisions 
--- a/Co2sobj_prop.thy	Tue May 21 08:01:33 2013 +0800
+++ b/Co2sobj_prop.thy	Tue May 21 10:19:51 2013 +0800
@@ -8,6 +8,8 @@
 
 (****************** cf2sfile path simpset ***************)
 
+thm cpfd2sfds_def
+
 lemma sroot_only:
   "cf2sfile s [] = Some sroot"
 by (simp add:cf2sfile_def)
--- a/Init_prop.thy	Tue May 21 08:01:33 2013 +0800
+++ b/Init_prop.thy	Tue May 21 10:19:51 2013 +0800
@@ -709,10 +709,11 @@
 apply (simp only:cpfd2sfds_def init_cfds2sfds_def)
 apply (rule set_eqI, rule iffI)
 apply (drule CollectD, rule CollectI, (erule exE)+)
-apply (rule_tac x = fd in exI, rule_tac x = sfd in exI, rule_tac x = f in exI) defer
+apply (rule_tac x = fd in exI, rule_tac x = f in exI) defer
 apply (drule CollectD, rule CollectI, (erule exE)+)
-apply (rule_tac x = fd in exI, rule_tac x = sfd in exI, rule_tac x = f in exI)
-using cfd2sfd_nil_prop by auto
+apply (rule_tac x = fd in exI, rule_tac x = f in exI)
+using cfd2sfd_nil_prop 
+by auto
 
 lemma ch2sshm_nil_prop:
   "h \<in> init_shms \<Longrightarrow> ch2sshm [] h = init_ch2sshm h"
--- a/ROOT	Tue May 21 08:01:33 2013 +0800
+++ b/ROOT	Tue May 21 10:19:51 2013 +0800
@@ -12,6 +12,8 @@
 session "alive" = "dynamic" + 
   options [document = false]
   theories
+    Static_type
+    Static
     Valid_prop
     Init_prop
     Current_files_prop
@@ -19,4 +21,4 @@
     Alive_prop
     Proc_fd_of_file_prop
     Finite_current
-    New_obj_prop
\ No newline at end of file
+    New_obj_prop
--- a/Static.thy	Tue May 21 08:01:33 2013 +0800
+++ b/Static.thy	Tue May 21 10:19:51 2013 +0800
@@ -47,7 +47,7 @@
 
 definition init_cfds2sfds :: "t_process \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) set"
 where
-  "init_cfds2sfds p \<equiv> { sfd. \<exists> fd sfd f. init_file_of_proc_fd p fd = Some f \<and> init_cfd2sfd p fd = Some sfd}"
+  "init_cfds2sfds p \<equiv> { sfd. \<exists> fd f. init_file_of_proc_fd p fd = Some f \<and> init_cfd2sfd p fd = Some sfd}"
 
 definition init_ch2sshm :: "t_shm \<Rightarrow> t_sshm option"
 where
@@ -58,7 +58,7 @@
 definition init_cph2spshs 
   :: "t_process \<Rightarrow> (t_sshm \<times> t_shm_attach_flag) set"
 where
-  "init_cph2spshs p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> init_procs_of_shm h \<and> 
+  "init_cph2spshs p \<equiv> {(sh, flag). \<exists> h. (p, flag) \<in> init_procs_of_shm h \<and> 
                                              init_ch2sshm h = Some sh}"
 
 definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option"
selinux