# HG changeset patch
# User chunhan
# Date 1377754172 -28800
# Node ID e7f850d1e08ee6ef7281eb5c36fbe58848a41e48
# Parent  6884b3c9284b0c0255dc5d08bc7147c4aacb056e
remove O_msg from co2sobj/init_obj2sobj

diff -r 6884b3c9284b -r e7f850d1e08e Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Thu Aug 29 10:01:24 2013 +0800
+++ b/Co2sobj_prop.thy	Thu Aug 29 13:29:32 2013 +0800
@@ -772,7 +772,7 @@
    \<Longrightarrow> cf2sfile (CloseFd p fd # s) f = cf2sfile s f"
 apply (frule vd_cons, frule vt_grant_os)
 apply (simp add:current_files_simps split:if_splits option.splits) 
-(* costs too much time, but solved
+(* costs too much time, but solved *)
 
 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps 
            split:if_splits option.splits  
@@ -780,8 +780,6 @@
                  not_deleted_init_file not_deleted_init_dir is_file_not_dir is_dir_not_file
             dest!:current_has_sec')
 done
-*)
-sorry
 
 lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other
   cf2sfile_unlink cf2sfile_rmdir cf2sfile_closefd
diff -r 6884b3c9284b -r e7f850d1e08e Current_prop.thy
--- a/Current_prop.thy	Thu Aug 29 10:01:24 2013 +0800
+++ b/Current_prop.thy	Thu Aug 29 13:29:32 2013 +0800
@@ -4,8 +4,6 @@
 begin
 (*>*)
 
-ML {*quick_and_dirty := true*}
-
 context flask begin
 
 lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"
diff -r 6884b3c9284b -r e7f850d1e08e ROOT
--- a/ROOT	Thu Aug 29 10:01:24 2013 +0800
+++ b/ROOT	Thu Aug 29 13:29:32 2013 +0800
@@ -22,3 +22,11 @@
     Proc_fd_of_file_prop
     Finite_current
     New_obj_prop
+
+session "co2sobj" = "alive" + 
+  options [document = false]
+  theories
+    Sectxt_prop
+    Delete_prop
+    Tainted_prop
+    Co2sobj_prop
\ No newline at end of file
diff -r 6884b3c9284b -r e7f850d1e08e S2ss_prop.thy
--- 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
diff -r 6884b3c9284b -r e7f850d1e08e Static.thy
--- a/Static.thy	Thu Aug 29 10:01:24 2013 +0800
+++ b/Static.thy	Thu Aug 29 13:29:32 2013 +0800
@@ -116,11 +116,11 @@
 | "init_obj2sobj (O_shm h) = 
      (case (init_ch2sshm h) of 
        Some sh \<Rightarrow> Some (S_shm sh)
-     | _       \<Rightarrow> None)"
+     | _       \<Rightarrow> None)"  (*
 | "init_obj2sobj (O_msg q m) = 
      (case (init_cq2smsgq q, init_cm2smsg q m) of 
         (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
-      | _                  \<Rightarrow> None)"
+      | _                  \<Rightarrow> None)" *)
 | "init_obj2sobj _ = None"
 
 definition  
diff -r 6884b3c9284b -r e7f850d1e08e Tainted_prop.thy
--- a/Tainted_prop.thy	Thu Aug 29 10:01:24 2013 +0800
+++ b/Tainted_prop.thy	Thu Aug 29 13:29:32 2013 +0800
@@ -2,6 +2,8 @@
 imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop Alive_prop
 begin
 
+ML {*quick_and_dirty := true*}
+
 context tainting begin
 
 fun Tainted :: "t_state \<Rightarrow> t_object set"