--- a/Flask.thy	Fri May 10 10:23:34 2013 +0800
+++ b/Flask.thy	Wed May 15 11:21:39 2013 +0800
@@ -207,7 +207,7 @@
 
 definition init_same_inode_files :: "t_file \<Rightarrow> t_file set"
 where
-  "init_same_inode_files f \<equiv> {f'. init_inum_of_file f = init_inum_of_file f'}"
+  "init_same_inode_files f \<equiv> if is_init_file f then {f'. init_inum_of_file f = init_inum_of_file f'} else {}"
 
 fun init_alive :: "t_object \<Rightarrow> bool"
 where
@@ -357,7 +357,7 @@
       | DGRAM  \<Rightarrow> (itag_of_inum \<tau>) (ino := Some Tag_UDP_SOCK) )"
 | "itag_of_inum (Accept p fd addr lport' fd' ino # \<tau>) = 
      (itag_of_inum \<tau>) (ino := Some Tag_TCP_SOCK)"
-| "itag_of_inum (_ # \<tau>) = itag_of_inum \<tau>"  (* may be sth wrong with nettemp representing addr \<times> netdev in statical analysis ??? *)
+| "itag_of_inum (_ # \<tau>) = itag_of_inum \<tau>"  
 
 definition is_file:: "t_state \<Rightarrow> t_file \<Rightarrow> bool"
 where
@@ -482,7 +482,7 @@
 
 definition same_inode_files :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file set"
 where
-  "same_inode_files s f \<equiv> {f'. inum_of_file s f = inum_of_file s f'}"
+  "same_inode_files s f \<equiv> if is_file s f then {f'. inum_of_file s f = inum_of_file s f'} else {}"
 
 fun flags_of_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_open_flags option"
 where
@@ -614,29 +614,28 @@
      case inumopt of
        Some ino \<Rightarrow>
     (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> 
-     (\<exists> pf. parent f = Some pf \<and> pf \<in> current_files \<tau> \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
+     (\<exists> pf. parent f = Some pf \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
      is_creat_flag flags \<and> fd \<notin> (current_proc_fds \<tau> p) \<and> ino \<notin> (current_inode_nums \<tau>))
    |   None     \<Rightarrow>
-    (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> \<not> is_creat_excl_flag flags \<and> is_file \<tau> f \<and>
+    (p \<in> current_procs \<tau> \<and> \<not> is_creat_excl_flag flags \<and> is_file \<tau> f \<and>
      fd \<notin> (current_proc_fds \<tau> p))           )"
 (*(if (is_dir \<tau> f) then (is_dir_flag flags \<and> \<not> is_write_flag flags) else (\<not> is_dir_flag flags)),
   here open is not applied to directories, readdir is for that, but it is not security-related *)
 | "os_grant \<tau> (CloseFd p fd)                  = 
     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p)"
 | "os_grant \<tau> (UnLink p f)                    = 
-    (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f \<and> f \<notin> files_hung_by_del \<tau>)"
+    (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> f \<notin> files_hung_by_del \<tau>)"
 | "os_grant \<tau> (Rmdir p f)                     = 
-    (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> dir_is_empty \<tau> f \<and> f \<notin> files_hung_by_del \<tau> \<and> f \<noteq> [])" (* root file cannot be deleted *)
+    (p \<in> current_procs \<tau> \<and> dir_is_empty \<tau> f \<and> f \<notin> files_hung_by_del \<tau> \<and> f \<noteq> [])" (* root file cannot be deleted *)
 | "os_grant \<tau> (Mkdir p f ino)                 = 
     (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> 
-     (\<exists> pf. parent f = Some pf \<and> pf \<in> current_files \<tau> \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
+     (\<exists> pf. parent f = Some pf \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
      ino \<notin> (current_inode_nums \<tau>))"
 | "os_grant \<tau> (LinkHard p f\<^isub>1 f\<^isub>2)              = 
-    (p \<in> current_procs \<tau> \<and> f\<^isub>1 \<in> current_files \<tau> \<and> f\<^isub>2 \<notin> current_files \<tau> \<and> 
-     (\<exists> pf\<^isub>2. parent f\<^isub>2 = Some pf\<^isub>2 \<and> pf\<^isub>2 \<in> current_files \<tau> \<and> is_dir \<tau> pf\<^isub>2 \<and> 
-             pf\<^isub>2 \<notin> files_hung_by_del \<tau>) \<and> is_file \<tau> f\<^isub>1)"
+    (p \<in> current_procs \<tau> \<and> is_file \<tau> f\<^isub>1 \<and> f\<^isub>2 \<notin> current_files \<tau> \<and> 
+     (\<exists> pf\<^isub>2. parent f\<^isub>2 = Some pf\<^isub>2 \<and> is_dir \<tau> pf\<^isub>2 \<and> pf\<^isub>2 \<notin> files_hung_by_del \<tau>))"
 | "os_grant \<tau> (Truncate p f len)              = 
-    (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f)"
+    (p \<in> current_procs \<tau> \<and> is_file \<tau> f)"
 (*
 | "os_grant \<tau> (FTruncate p fd len)            = 
     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> 
@@ -652,7 +651,7 @@
      (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and> 
      (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))"
 | "os_grant \<tau> (Execve p f fds)                = 
-    (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> current_proc_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} *)
+    (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> current_proc_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} *)
 (*
 | "os_grant \<tau> (Rename p f\<^isub>2 f\<^isub>3)                = 
     (p \<in> current_procs \<tau> \<and> f\<^isub>2 \<in> current_files \<tau> \<and> \<not>(f\<^isub>2 \<preceq> f\<^isub>3) \<and> f\<^isub>3 \<notin> current_files \<tau> \<and>
@@ -689,8 +688,8 @@
     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> 
      socket_state \<tau> (p, fd) = Some SS_bind)"
 | "os_grant \<tau> (Listen p fd)                   = 
-    (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> 
-     socket_state \<tau> (p, fd) = Some SS_bind \<and> is_tcp_sock \<tau> (p, fd))" (* Listen and Accept should only be used for TCP sever side *)
+    (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> is_tcp_sock \<tau> (p, fd) \<and>
+     socket_state \<tau> (p, fd) = Some SS_bind)" (* Listen and Accept should only be used for TCP sever side *)
 | "os_grant \<tau> (SendSock p fd)                 = 
     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> 
      socket_in_sending \<tau> (p, fd))"
@@ -716,12 +715,12 @@
 fun alive :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"
 where
   "alive s (O_proc p)     = (p \<in> current_procs s)"
-| "alive s (O_file f)     = (f \<in> current_files s \<and> is_file s f)"
-| "alive s (O_dir  f)     = (f \<in> current_files s \<and> is_dir s f)"
+| "alive s (O_file f)     = (is_file s f)"
+| "alive s (O_dir  f)     = (is_dir s f)"
 | "alive s (O_fd p fd)    = (fd \<in> current_proc_fds s p)"
 | "alive s (O_node n)     = (n \<in> init_nodes)"
-| "alive s (O_tcp_sock k) = (k \<in> current_sockets s \<and> is_tcp_sock s k)"
-| "alive s (O_udp_sock k) = (k \<in> current_sockets s \<and> is_udp_sock s k)"
+| "alive s (O_tcp_sock k) = (is_tcp_sock s k)"
+| "alive s (O_udp_sock k) = (is_udp_sock s k)"
 | "alive s (O_shm  h)     = (h \<in> current_shms s)"
 | "alive s (O_msgq q)     = (q \<in> current_msgqs s)"
 | "alive s (O_msg q m)    = (m \<in> set (msgs_of_queue s q) \<and> q \<in> current_msgqs s)"