equal
deleted
inserted
replaced
690 | "os_grant \<tau> (WriteFile p fd) = |
690 | "os_grant \<tau> (WriteFile p fd) = |
691 (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> |
691 (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> |
692 (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and> |
692 (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and> |
693 (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))" |
693 (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))" |
694 | "os_grant \<tau> (Execve p f fds) = |
694 | "os_grant \<tau> (Execve p f fds) = |
695 (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> current_proc_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} *) |
695 (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> proc_file_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} \<and> fds \<subseteq> current_proc_fds \<tau> p *) |
696 (* |
696 (* |
697 | "os_grant \<tau> (Rename p f\<^isub>2 f\<^isub>3) = |
697 | "os_grant \<tau> (Rename p f\<^isub>2 f\<^isub>3) = |
698 (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> |
698 (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> |
699 (\<exists> pf\<^isub>3. parent f\<^isub>3 = Some pf\<^isub>3 \<and> pf\<^isub>3 \<in> current_files \<tau> \<and> is_dir \<tau> pf\<^isub>3 \<and> |
699 (\<exists> pf\<^isub>3. parent f\<^isub>3 = Some pf\<^isub>3 \<and> pf\<^isub>3 \<in> current_files \<tau> \<and> is_dir \<tau> pf\<^isub>3 \<and> |
700 pf\<^isub>3 \<notin> files_hung_by_del \<tau>) )" |
700 pf\<^isub>3 \<notin> files_hung_by_del \<tau>) )" |
742 socket_in_trans \<tau> (p, fd))" |
742 socket_in_trans \<tau> (p, fd))" |
743 (* |
743 (* |
744 | "os_grant \<tau> (ChangeOwner p u) = (p \<in> current_procs \<tau> \<and> u \<in> current_users \<tau>)" |
744 | "os_grant \<tau> (ChangeOwner p u) = (p \<in> current_procs \<tau> \<and> u \<in> current_users \<tau>)" |
745 *) |
745 *) |
746 | "os_grant \<tau> (Clone p p' fds shms) = |
746 | "os_grant \<tau> (Clone p p' fds shms) = |
747 (p \<in> current_procs \<tau> \<and> p' \<notin> (current_procs \<tau>) \<and> fds \<subseteq> current_proc_fds \<tau> p \<and> |
747 (p \<in> current_procs \<tau> \<and> p' \<notin> (current_procs \<tau>) \<and> fds \<subseteq> proc_file_fds \<tau> p \<and> |
748 (\<forall> h \<in> shms. \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))" |
748 (\<forall> h \<in> shms. \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))" (* current_proc_fds \<rightarrow> proc_file_fds *) |
749 | "os_grant \<tau> (Kill p\<^isub>1 p\<^isub>2) = |
749 | "os_grant \<tau> (Kill p\<^isub>1 p\<^isub>2) = |
750 (p\<^isub>1 \<in> current_procs \<tau> \<and> p\<^isub>2 \<in> current_procs \<tau>)" (* a process can kill itself right? *) |
750 (p\<^isub>1 \<in> current_procs \<tau> \<and> p\<^isub>2 \<in> current_procs \<tau>)" (* a process can kill itself right? *) |
751 | "os_grant \<tau> (Exit p) = |
751 | "os_grant \<tau> (Exit p) = |
752 (p \<in> current_procs \<tau>)" |
752 (p \<in> current_procs \<tau>)" |
753 | "os_grant \<tau> (Ptrace p\<^isub>1 p\<^isub>2) = |
753 | "os_grant \<tau> (Ptrace p\<^isub>1 p\<^isub>2) = |